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  559  reximddv  2609  rexlimdvaa  2624  issod  4366  ordsuc  4611  fcof1  5852  riota5f  5924  ovmpodf  6077  tfrlemi1  6418  eqsuptid  7099  eqinftid  7123  ordiso2  7137  addnq0mo  7560  mulnq0mo  7561  genprndl  7634  genprndu  7635  addlocpr  7649  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemfl  7722  ltexprlemfu  7724  aptiprleml  7752  caucvgprprlemexbt  7819  addsrmo  7856  mulsrmo  7857  prodge0  8927  un0addcl  9328  un0mulcl  9329  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  seq3split  10633  seqsplitg  10634  seqf1oglem1  10664  seq3id2  10671  seqhomog  10675  expnegzap  10718  expcanlem  10860  bcval5  10908  seq3coll  10987  caucvgrelemcau  11291  cau3lem  11425  reccn2ap  11624  summodclem2  11693  zsumdc  11695  fsumf1o  11701  fisumss  11703  fsumcl2lem  11709  fsumadd  11717  fisum0diag2  11758  fsummulc2  11759  mertenslem2  11847  prodmodclem2  11888  zproddc  11890  fprodseq  11894  fprodf1o  11899  prodssdc  11900  fprodssdc  11901  fprodmul  11902  dvds0lem  12112  dvdsnegb  12119  dvdssub2  12146  isprm6  12469  hashgcdeq  12562  modprminv  12572  modprminveq  12573  reumodprminv  12576  pcqmul  12626  pcqcl  12629  pcxnn0cl  12633  pcxcl  12634  pc2dvds  12653  pcadd  12663  pcmpt  12666  pockthg  12680  infpnlem1  12682  mgmidsssn0  13216  mhmeql  13324  grprcan  13369  dfgrp3mlem  13430  mulgnn0ass  13494  isnsg3  13543  ghmpreima  13602  ghmeql  13603  lss1d  14145  znidomb  14420  topssnei  14634  innei  14635  cnptopco  14694  cncnpi  14700  cncnp  14702  cnconst2  14705  cnpdis  14714  lmtopcnp  14722  tx2cn  14742  txdis  14749  blssps  14899  blss  14900  neibl  14963  metss  14966  metequiv2  14968  metrest  14978  metcnp3  14983  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemloc  15113  plycolemc  15230  mpodvdsmulf1o  15462  perfectlem2  15472  2sqlem5  15596  2sqlem6  15597  2sqlem8  15600  2sqlem10  15602  nconstwlpolem  16004