Theorem expr 375

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

Step	Hyp	Ref	Expression
1		expr.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 365	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  animpimp2impd  561  reximddv  2636  rexlimdvaa  2652  issod  4422  ordsuc  4667  fcof1  5934  riota5f  6008  ovmpodf  6163  suppssdc  6438  tfrlemi1  6541  eqsuptid  7239  eqinftid  7263  ordiso2  7277  addnq0mo  7710  mulnq0mo  7711  genprndl  7784  genprndu  7785  addlocpr  7799  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemfl  7872  ltexprlemfu  7874  aptiprleml  7902  caucvgprprlemexbt  7969  addsrmo  8006  mulsrmo  8007  prodge0  9076  un0addcl  9477  un0mulcl  9478  seq3fveq2  10783  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  monoord  10793  seq3split  10796  seqsplitg  10797  seqf1oglem1  10827  seq3id2  10834  seqhomog  10838  expnegzap  10881  expcanlem  11023  bcval5  11071  seq3coll  11152  wrdind  11352  wrd2ind  11353  caucvgrelemcau  11603  cau3lem  11737  reccn2ap  11936  summodclem2  12006  zsumdc  12008  fsumf1o  12014  fisumss  12016  fsumcl2lem  12022  fsumadd  12030  fisum0diag2  12071  fsummulc2  12072  mertenslem2  12160  prodmodclem2  12201  zproddc  12203  fprodseq  12207  fprodf1o  12212  prodssdc  12213  fprodssdc  12214  fprodmul  12215  dvds0lem  12425  dvdsnegb  12432  dvdssub2  12459  isprm6  12782  hashgcdeq  12875  modprminv  12885  modprminveq  12886  reumodprminv  12889  pcqmul  12939  pcqcl  12942  pcxnn0cl  12946  pcxcl  12947  pc2dvds  12966  pcadd  12976  pcmpt  12979  pockthg  12993  infpnlem1  12995  mgmidsssn0  13530  mhmeql  13638  grprcan  13683  dfgrp3mlem  13744  mulgnn0ass  13808  isnsg3  13857  ghmpreima  13916  ghmeql  13917  lss1d  14462  znidomb  14737  topssnei  14956  innei  14957  cnptopco  15016  cncnpi  15022  cncnp  15024  cnconst2  15027  cnpdis  15036  lmtopcnp  15044  tx2cn  15064  txdis  15071  blssps  15221  blss  15222  neibl  15285  metss  15288  metequiv2  15290  metrest  15300  metcnp3  15305  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemloc  15435  plycolemc  15552  mpodvdsmulf1o  15787  perfectlem2  15797  2sqlem5  15921  2sqlem6  15922  2sqlem8  15925  2sqlem10  15927  nconstwlpolem  16781