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

Theorem expr 373
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 363 . 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  549  reximddv  2567  rexlimdvaa  2582  issod  4294  ordsuc  4537  fcof1  5748  riota5f  5819  ovmpodf  5967  tfrlemi1  6294  eqsuptid  6956  eqinftid  6980  ordiso2  6994  addnq0mo  7382  mulnq0mo  7383  genprndl  7456  genprndu  7457  addlocpr  7471  ltexprlemm  7535  ltexprlemopl  7536  ltexprlemopu  7538  ltexprlemfl  7544  ltexprlemfu  7546  aptiprleml  7574  caucvgprprlemexbt  7641  addsrmo  7678  mulsrmo  7679  prodge0  8743  un0addcl  9141  un0mulcl  9142  seq3fveq2  10398  seq3shft2  10402  monoord  10405  seq3split  10408  seq3id2  10438  expnegzap  10483  expcanlem  10622  bcval5  10670  seq3coll  10749  caucvgrelemcau  10916  cau3lem  11050  reccn2ap  11248  summodclem2  11317  zsumdc  11319  fsumf1o  11325  fisumss  11327  fsumcl2lem  11333  fsumadd  11341  fisum0diag2  11382  fsummulc2  11383  mertenslem2  11471  prodmodclem2  11512  zproddc  11514  fprodseq  11518  fprodf1o  11523  prodssdc  11524  fprodssdc  11525  fprodmul  11526  dvds0lem  11735  dvdsnegb  11742  dvdssub2  11769  isprm6  12073  hashgcdeq  12165  modprminv  12175  modprminveq  12176  reumodprminv  12179  pcqmul  12229  pcqcl  12232  pcxnn0cl  12236  pcxcl  12237  pc2dvds  12255  pcadd  12265  pcmpt  12267  pockthg  12281  infpnlem1  12283  topssnei  12760  innei  12761  cnptopco  12820  cncnpi  12826  cncnp  12828  cnconst2  12831  cnpdis  12840  lmtopcnp  12848  tx2cn  12868  txdis  12875  blssps  13025  blss  13026  neibl  13089  metss  13092  metequiv2  13094  metrest  13104  metcnp3  13109  ivthinclemlopn  13212  ivthinclemlr  13213  ivthinclemuopn  13214  ivthinclemur  13215  ivthinclemloc  13217  nconstwlpolem  13836
  Copyright terms: Public domain W3C validator