Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exp45 Structured version   GIF version

Theorem exp45 356
 Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp45.1 ((φ (ψ (χ θ))) → τ)
Assertion
Ref Expression
exp45 (φ → (ψ → (χ → (θτ))))

Proof of Theorem exp45
StepHypRef Expression
1 exp45.1 . . 3 ((φ (ψ (χ θ))) → τ)
21exp32 347 . 2 (φ → (ψ → ((χ θ) → τ)))
32exp4a 348 1 (φ → (ψ → (χ → (θτ))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator
{"ft_lang_label":"__label__en","ft_lang_prob":0.6258737,"math_prob":0.7961607,"size":791,"snap":"2020-45-2020-50","text_gpt3_token_len":310,"char_repetition_ratio":0.10673443,"word_repetition_ratio":0.16025642,"special_character_ratio":0.42857143,"punctuation_ratio":0.10666667,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99264836,"pos_list":[0,1,2],"im_url_duplicate_count":[null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-12-02T12:27:57Z\",\"WARC-Record-ID\":\"<urn:uuid:58e1d3ed-e5e0-452a-b8be-41006ee2853c>\",\"Content-Length\":\"8156\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:e3e7ae7b-cc07-43de-9603-ec0c5524ccf6>\",\"WARC-Concurrent-To\":\"<urn:uuid:8124f8ba-b1da-4a91-97ff-9d7c8ace7035>\",\"WARC-IP-Address\":\"78.47.47.15\",\"WARC-Target-URI\":\"http://at.metamath.org/ileuni/exp45.html\",\"WARC-Payload-Digest\":\"sha1:WONBRKJEEGVWO6WAMRET2HXKAO3UGDZ2\",\"WARC-Block-Digest\":\"sha1:QYM4GSZJ7LO3YY7EHOOFFK4WZ6X5RGUC\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-50/CC-MAIN-2020-50_segments_1606141708017.73_warc_CC-MAIN-20201202113815-20201202143815-00490.warc.gz\"}"}