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  4466  ordsuc  4712  fcof1  5992  riota5f  6068  ovmpodf  6223  suppssdc  6504  tfrlemi1  6608  eqsuptid  7343  eqinftid  7367  ordiso2  7381  addnq0mo  7820  mulnq0mo  7821  genprndl  7894  genprndu  7895  addlocpr  7909  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemfl  7982  ltexprlemfu  7984  aptiprleml  8012  caucvgprprlemexbt  8079  addsrmo  8116  mulsrmo  8117  prodge0  9192  un0addcl  9607  un0mulcl  9608  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  seq3split  10945  seqsplitg  10946  seqf1oglem1  10976  seq3id2  10983  seqhomog  10987  expnegzap  11030  expcanlem  11174  bcval5  11222  hashfibc  11304  seq3coll  11315  wrdind  11515  wrd2ind  11516  caucvgrelemcau  11767  cau3lem  11902  reccn2ap  12103  summodclem2  12173  zsumdc  12175  fsumf1o  12181  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  fisum0diag2  12238  fsummulc2  12239  mertenslem2  12327  prodmodclem2  12368  zproddc  12370  fprodseq  12374  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodmul  12382  dvds0lem  12592  dvdsnegb  12599  dvdssub2  12626  isprm6  12950  hashgcdeq  13046  modprminv  13056  modprminveq  13057  reumodprminv  13060  pcqmul  13110  pcqcl  13113  pcxnn0cl  13117  pcxcl  13118  pc2dvds  13137  pcadd  13147  pcmpt  13150  pockthg  13164  infpnlem1  13166  ballotfilemfc0  13289  ballotfilemfcc  13290  mgmidsssn0  13762  mhmeql  13857  grprcan  13900  dfgrp3mlem  13961  mulgnn0ass  14019  isnsg3  14068  ghmpreima  14127  ghmeql  14128  lss1d  14828  znidomb  15101  rnasclassa  15146  mvrf1fi  15219  topssnei  15405  innei  15406  cnptopco  15465  cncnpi  15471  cncnp  15473  cnconst2  15476  cnpdis  15485  lmtopcnp  15493  tx2cn  15513  txdis  15520  blssps  15670  blss  15671  neibl  15734  metss  15737  metequiv2  15739  metrest  15749  metcnp3  15754  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  plycolemc  16001  rpcxpmul2z  16165  ppinprm  16277  chtnprm  16279  mpodvdsmulf1o  16301  chtublem  16312  perfectlem2  16317  bposlem1  16328  bposlem3  16330  2sqlem5  16460  2sqlem6  16461  2sqlem8  16464  2sqlem10  16466  nconstwlpolem  17339