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  2610  rexlimdvaa  2625  issod  4379  ordsuc  4624  fcof1  5870  riota5f  5942  ovmpodf  6095  tfrlemi1  6436  eqsuptid  7120  eqinftid  7144  ordiso2  7158  addnq0mo  7590  mulnq0mo  7591  genprndl  7664  genprndu  7665  addlocpr  7679  ltexprlemm  7743  ltexprlemopl  7744  ltexprlemopu  7746  ltexprlemfl  7752  ltexprlemfu  7754  aptiprleml  7782  caucvgprprlemexbt  7849  addsrmo  7886  mulsrmo  7887  prodge0  8957  un0addcl  9358  un0mulcl  9359  seq3fveq2  10652  seqfveq2g  10654  seq3shft2  10658  seqshft2g  10659  monoord  10662  seq3split  10665  seqsplitg  10666  seqf1oglem1  10696  seq3id2  10703  seqhomog  10707  expnegzap  10750  expcanlem  10892  bcval5  10940  seq3coll  11019  wrdind  11208  wrd2ind  11209  caucvgrelemcau  11376  cau3lem  11510  reccn2ap  11709  summodclem2  11778  zsumdc  11780  fsumf1o  11786  fisumss  11788  fsumcl2lem  11794  fsumadd  11802  fisum0diag2  11843  fsummulc2  11844  mertenslem2  11932  prodmodclem2  11973  zproddc  11975  fprodseq  11979  fprodf1o  11984  prodssdc  11985  fprodssdc  11986  fprodmul  11987  dvds0lem  12197  dvdsnegb  12204  dvdssub2  12231  isprm6  12554  hashgcdeq  12647  modprminv  12657  modprminveq  12658  reumodprminv  12661  pcqmul  12711  pcqcl  12714  pcxnn0cl  12718  pcxcl  12719  pc2dvds  12738  pcadd  12748  pcmpt  12751  pockthg  12765  infpnlem1  12767  mgmidsssn0  13301  mhmeql  13409  grprcan  13454  dfgrp3mlem  13515  mulgnn0ass  13579  isnsg3  13628  ghmpreima  13687  ghmeql  13688  lss1d  14230  znidomb  14505  topssnei  14719  innei  14720  cnptopco  14779  cncnpi  14785  cncnp  14787  cnconst2  14790  cnpdis  14799  lmtopcnp  14807  tx2cn  14827  txdis  14834  blssps  14984  blss  14985  neibl  15048  metss  15051  metequiv2  15053  metrest  15063  metcnp3  15068  ivthinclemlopn  15193  ivthinclemlr  15194  ivthinclemuopn  15195  ivthinclemur  15196  ivthinclemloc  15198  plycolemc  15315  mpodvdsmulf1o  15547  perfectlem2  15557  2sqlem5  15681  2sqlem6  15682  2sqlem8  15685  2sqlem10  15687  nconstwlpolem  16176