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  2600  rexlimdvaa  2615  issod  4355  ordsuc  4600  fcof1  5833  riota5f  5905  ovmpodf  6058  tfrlemi1  6399  eqsuptid  7072  eqinftid  7096  ordiso2  7110  addnq0mo  7533  mulnq0mo  7534  genprndl  7607  genprndu  7608  addlocpr  7622  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemfl  7695  ltexprlemfu  7697  aptiprleml  7725  caucvgprprlemexbt  7792  addsrmo  7829  mulsrmo  7830  prodge0  8900  un0addcl  9301  un0mulcl  9302  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seqf1oglem1  10630  seq3id2  10637  seqhomog  10641  expnegzap  10684  expcanlem  10826  bcval5  10874  seq3coll  10953  caucvgrelemcau  11164  cau3lem  11298  reccn2ap  11497  summodclem2  11566  zsumdc  11568  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumadd  11590  fisum0diag2  11631  fsummulc2  11632  mertenslem2  11720  prodmodclem2  11761  zproddc  11763  fprodseq  11767  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodmul  11775  dvds0lem  11985  dvdsnegb  11992  dvdssub2  12019  isprm6  12342  hashgcdeq  12435  modprminv  12445  modprminveq  12446  reumodprminv  12449  pcqmul  12499  pcqcl  12502  pcxnn0cl  12506  pcxcl  12507  pc2dvds  12526  pcadd  12536  pcmpt  12539  pockthg  12553  infpnlem1  12555  mgmidsssn0  13088  mhmeql  13196  grprcan  13241  dfgrp3mlem  13302  mulgnn0ass  13366  isnsg3  13415  ghmpreima  13474  ghmeql  13475  lss1d  14017  znidomb  14292  topssnei  14484  innei  14485  cnptopco  14544  cncnpi  14550  cncnp  14552  cnconst2  14555  cnpdis  14564  lmtopcnp  14572  tx2cn  14592  txdis  14599  blssps  14749  blss  14750  neibl  14813  metss  14816  metequiv2  14818  metrest  14828  metcnp3  14833  ivthinclemlopn  14958  ivthinclemlr  14959  ivthinclemuopn  14960  ivthinclemur  14961  ivthinclemloc  14963  plycolemc  15080  mpodvdsmulf1o  15312  perfectlem2  15322  2sqlem5  15446  2sqlem6  15447  2sqlem8  15450  2sqlem10  15452  nconstwlpolem  15800