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

Theorem expr 367
 Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
expr.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
expr ((𝜑𝜓) → (𝜒𝜃))

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21exp32 357 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 122 1 ((𝜑𝜓) → (𝜒𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem is referenced by:  reximddv  2465  rexlimdvaa  2479  issod  4082  ordsuc  4314  fcof1  5454  riota5f  5523  ovmpt2df  5663  tfrlemi1  5981  eqsuptid  6469  eqinftid  6493  ordiso2  6505  addnq0mo  6699  mulnq0mo  6700  genprndl  6773  genprndu  6774  addlocpr  6788  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemfl  6861  ltexprlemfu  6863  aptiprleml  6891  caucvgprprlemexbt  6958  addsrmo  6982  mulsrmo  6983  prodge0  7999  un0addcl  8388  un0mulcl  8389  iseqfveq2  9544  iseqshft2  9548  monoord  9551  iseqsplit  9554  iseqid2  9564  expnegzap  9607  expcanlem  9740  ibcval5  9787  caucvgrelemcau  10004  cau3lem  10138  dvds0lem  10350  dvdsnegb  10357  dvdssub2  10382  isprm6  10670
 Copyright terms: Public domain W3C validator