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

Theorem exp32 363
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp32.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
exp32 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21ex 114 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 256 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  exp44  371  exp45  372  expr  373  anassrs  398  an13s  562  3impb  1194  xordidc  1394  f0rn0  5392  funfvima3  5729  isoini  5797  ovg  5991  fundmen  6784  distrlem1prl  7544  distrlem1pru  7545  caucvgprprlemaddq  7670  recexgt0sr  7735  axpre-suploclemres  7863  cnegexlem2  8095  mulgt1  8779  faclbnd  10675  divgcdcoprm0  12055  cncongr2  12058  oddpwdclemdvds  12124  oddpwdclemndvds  12125  infpnlem1  12311  cnpnei  13013  zabsle1  13694
  Copyright terms: Public domain W3C validator