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

Theorem expr 372
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 362 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 123 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-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  animpimp2impd  548  reximddv  2535  rexlimdvaa  2550  issod  4241  ordsuc  4478  fcof1  5684  riota5f  5754  ovmpodf  5902  tfrlemi1  6229  eqsuptid  6884  eqinftid  6908  ordiso2  6920  addnq0mo  7267  mulnq0mo  7268  genprndl  7341  genprndu  7342  addlocpr  7356  ltexprlemm  7420  ltexprlemopl  7421  ltexprlemopu  7423  ltexprlemfl  7429  ltexprlemfu  7431  aptiprleml  7459  caucvgprprlemexbt  7526  addsrmo  7563  mulsrmo  7564  prodge0  8624  un0addcl  9022  un0mulcl  9023  seq3fveq2  10254  seq3shft2  10258  monoord  10261  seq3split  10264  seq3id2  10294  expnegzap  10339  expcanlem  10474  bcval5  10521  seq3coll  10597  caucvgrelemcau  10764  cau3lem  10898  reccn2ap  11094  summodclem2  11163  zsumdc  11165  fsumf1o  11171  fisumss  11173  fsumcl2lem  11179  fsumadd  11187  fisum0diag2  11228  fsummulc2  11229  mertenslem2  11317  prodmodclem2  11358  dvds0lem  11514  dvdsnegb  11521  dvdssub2  11546  isprm6  11836  hashgcdeq  11915  topssnei  12345  innei  12346  cnptopco  12405  cncnpi  12411  cncnp  12413  cnconst2  12416  cnpdis  12425  lmtopcnp  12433  tx2cn  12453  txdis  12460  blssps  12610  blss  12611  neibl  12674  metss  12677  metequiv2  12679  metrest  12689  metcnp3  12694  ivthinclemlopn  12797  ivthinclemlr  12798  ivthinclemuopn  12799  ivthinclemur  12800  ivthinclemloc  12802
  Copyright terms: Public domain W3C validator