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 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  animpimp2impd  565  reximddv  2653  rexlimdvaa  2669  issod  4464  ordsuc  4710  fcof1  5989  riota5f  6065  ovmpodf  6220  suppssdc  6500  tfrlemi1  6603  eqsuptid  7338  eqinftid  7362  ordiso2  7376  addnq0mo  7815  mulnq0mo  7816  genprndl  7889  genprndu  7890  addlocpr  7904  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemfl  7977  ltexprlemfu  7979  aptiprleml  8007  caucvgprprlemexbt  8074  addsrmo  8111  mulsrmo  8112  prodge0  9187  un0addcl  9601  un0mulcl  9602  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  seqf1oglem1  10971  seq3id2  10978  seqhomog  10982  expnegzap  11025  expcanlem  11169  bcval5  11217  hashfibc  11299  seq3coll  11310  wrdind  11510  wrd2ind  11511  caucvgrelemcau  11762  cau3lem  11897  reccn2ap  12098  summodclem2  12168  zsumdc  12170  fsumf1o  12176  fisumss  12178  fsumcl2lem  12184  fsumadd  12192  fisum0diag2  12233  fsummulc2  12234  mertenslem2  12322  prodmodclem2  12363  zproddc  12365  fprodseq  12369  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodmul  12377  dvds0lem  12587  dvdsnegb  12594  dvdssub2  12621  isprm6  12945  hashgcdeq  13041  modprminv  13051  modprminveq  13052  reumodprminv  13055  pcqmul  13105  pcqcl  13108  pcxnn0cl  13112  pcxcl  13113  pc2dvds  13132  pcadd  13142  pcmpt  13145  pockthg  13159  infpnlem1  13161  ballotfilemfc0  13284  ballotfilemfcc  13285  mgmidsssn0  13757  mhmeql  13852  grprcan  13895  dfgrp3mlem  13956  mulgnn0ass  14014  isnsg3  14063  ghmpreima  14122  ghmeql  14123  lss1d  14804  znidomb  15077  rnasclassa  15122  topssnei  15354  innei  15355  cnptopco  15414  cncnpi  15420  cncnp  15422  cnconst2  15425  cnpdis  15434  lmtopcnp  15442  tx2cn  15462  txdis  15469  blssps  15619  blss  15620  neibl  15683  metss  15686  metequiv2  15688  metrest  15698  metcnp3  15703  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  plycolemc  15950  ppinprm  16221  chtnprm  16223  mpodvdsmulf1o  16245  chtublem  16256  perfectlem2  16261  bposlem1  16272  bposlem3  16274  2sqlem5  16404  2sqlem6  16405  2sqlem8  16408  2sqlem10  16410  nconstwlpolem  17282