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  7337  eqinftid  7361  ordiso2  7375  addnq0mo  7814  mulnq0mo  7815  genprndl  7888  genprndu  7889  addlocpr  7903  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemfu  7978  aptiprleml  8006  caucvgprprlemexbt  8073  addsrmo  8110  mulsrmo  8111  prodge0  9186  un0addcl  9600  un0mulcl  9601  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  seq3split  10938  seqsplitg  10939  seqf1oglem1  10969  seq3id2  10976  seqhomog  10980  expnegzap  11023  expcanlem  11167  bcval5  11215  hashfibc  11297  seq3coll  11308  wrdind  11508  wrd2ind  11509  caucvgrelemcau  11760  cau3lem  11895  reccn2ap  12095  summodclem2  12165  zsumdc  12167  fsumf1o  12173  fisumss  12175  fsumcl2lem  12181  fsumadd  12189  fisum0diag2  12230  fsummulc2  12231  mertenslem2  12319  prodmodclem2  12360  zproddc  12362  fprodseq  12366  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodmul  12374  dvds0lem  12584  dvdsnegb  12591  dvdssub2  12618  isprm6  12942  hashgcdeq  13038  modprminv  13048  modprminveq  13049  reumodprminv  13052  pcqmul  13102  pcqcl  13105  pcxnn0cl  13109  pcxcl  13110  pc2dvds  13129  pcadd  13139  pcmpt  13142  pockthg  13156  infpnlem1  13158  ballotfilemfc0  13281  ballotfilemfcc  13282  mgmidsssn0  13753  mhmeql  13848  grprcan  13891  dfgrp3mlem  13952  mulgnn0ass  14010  isnsg3  14059  ghmpreima  14118  ghmeql  14119  lss1d  14769  znidomb  15042  rnasclassa  15087  topssnei  15312  innei  15313  cnptopco  15372  cncnpi  15378  cncnp  15380  cnconst2  15383  cnpdis  15392  lmtopcnp  15400  tx2cn  15420  txdis  15427  blssps  15577  blss  15578  neibl  15641  metss  15644  metequiv2  15646  metrest  15656  metcnp3  15661  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  plycolemc  15908  ppinprm  16171  mpodvdsmulf1o  16185  perfectlem2  16198  bposlem1  16209  bposlem3  16211  2sqlem5  16336  2sqlem6  16337  2sqlem8  16340  2sqlem10  16342  nconstwlpolem  17213