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  2635  rexlimdvaa  2651  issod  4416  ordsuc  4661  fcof1  5923  riota5f  5997  ovmpodf  6152  tfrlemi1  6497  eqsuptid  7195  eqinftid  7219  ordiso2  7233  addnq0mo  7666  mulnq0mo  7667  genprndl  7740  genprndu  7741  addlocpr  7755  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemfl  7828  ltexprlemfu  7830  aptiprleml  7858  caucvgprprlemexbt  7925  addsrmo  7962  mulsrmo  7963  prodge0  9033  un0addcl  9434  un0mulcl  9435  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  seq3split  10749  seqsplitg  10750  seqf1oglem1  10780  seq3id2  10787  seqhomog  10791  expnegzap  10834  expcanlem  10976  bcval5  11024  seq3coll  11105  wrdind  11302  wrd2ind  11303  caucvgrelemcau  11540  cau3lem  11674  reccn2ap  11873  summodclem2  11942  zsumdc  11944  fsumf1o  11950  fisumss  11952  fsumcl2lem  11958  fsumadd  11966  fisum0diag2  12007  fsummulc2  12008  mertenslem2  12096  prodmodclem2  12137  zproddc  12139  fprodseq  12143  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodmul  12151  dvds0lem  12361  dvdsnegb  12368  dvdssub2  12395  isprm6  12718  hashgcdeq  12811  modprminv  12821  modprminveq  12822  reumodprminv  12825  pcqmul  12875  pcqcl  12878  pcxnn0cl  12882  pcxcl  12883  pc2dvds  12902  pcadd  12912  pcmpt  12915  pockthg  12929  infpnlem1  12931  mgmidsssn0  13466  mhmeql  13574  grprcan  13619  dfgrp3mlem  13680  mulgnn0ass  13744  isnsg3  13793  ghmpreima  13852  ghmeql  13853  lss1d  14396  znidomb  14671  topssnei  14885  innei  14886  cnptopco  14945  cncnpi  14951  cncnp  14953  cnconst2  14956  cnpdis  14965  lmtopcnp  14973  tx2cn  14993  txdis  15000  blssps  15150  blss  15151  neibl  15214  metss  15217  metequiv2  15219  metrest  15229  metcnp3  15234  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  plycolemc  15481  mpodvdsmulf1o  15713  perfectlem2  15723  2sqlem5  15847  2sqlem6  15848  2sqlem8  15851  2sqlem10  15853  nconstwlpolem  16669