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  2645  rexlimdvaa  2661  issod  4440  ordsuc  4685  fcof1  5956  riota5f  6030  ovmpodf  6185  suppssdc  6460  tfrlemi1  6563  eqsuptid  7288  eqinftid  7312  ordiso2  7326  addnq0mo  7762  mulnq0mo  7763  genprndl  7836  genprndu  7837  addlocpr  7851  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemfl  7924  ltexprlemfu  7926  aptiprleml  7954  caucvgprprlemexbt  8021  addsrmo  8058  mulsrmo  8059  prodge0  9128  un0addcl  9529  un0mulcl  9530  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  monoord  10847  seq3split  10850  seqsplitg  10851  seqf1oglem1  10881  seq3id2  10888  seqhomog  10892  expnegzap  10935  expcanlem  11077  bcval5  11125  hashfibc  11207  seq3coll  11214  wrdind  11414  wrd2ind  11415  caucvgrelemcau  11665  cau3lem  11799  reccn2ap  11998  summodclem2  12068  zsumdc  12070  fsumf1o  12076  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  fisum0diag2  12133  fsummulc2  12134  mertenslem2  12222  prodmodclem2  12263  zproddc  12265  fprodseq  12269  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodmul  12277  dvds0lem  12487  dvdsnegb  12494  dvdssub2  12521  isprm6  12844  hashgcdeq  12937  modprminv  12947  modprminveq  12948  reumodprminv  12951  pcqmul  13001  pcqcl  13004  pcxnn0cl  13008  pcxcl  13009  pc2dvds  13028  pcadd  13038  pcmpt  13041  pockthg  13055  infpnlem1  13057  mgmidsssn0  13597  mhmeql  13705  grprcan  13750  dfgrp3mlem  13811  mulgnn0ass  13875  isnsg3  13924  ghmpreima  13983  ghmeql  13984  lss1d  14531  znidomb  14806  topssnei  15027  innei  15028  cnptopco  15087  cncnpi  15093  cncnp  15095  cnconst2  15098  cnpdis  15107  lmtopcnp  15115  tx2cn  15135  txdis  15142  blssps  15292  blss  15293  neibl  15356  metss  15359  metequiv2  15361  metrest  15371  metcnp3  15376  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemloc  15506  plycolemc  15623  mpodvdsmulf1o  15858  perfectlem2  15868  2sqlem5  15992  2sqlem6  15993  2sqlem8  15996  2sqlem10  15998  nconstwlpolem  16851