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  565  reximddv  2653  rexlimdvaa  2669  issod  4459  ordsuc  4705  fcof1  5979  riota5f  6055  ovmpodf  6210  suppssdc  6490  tfrlemi1  6593  eqsuptid  7327  eqinftid  7351  ordiso2  7365  addnq0mo  7804  mulnq0mo  7805  genprndl  7878  genprndu  7879  addlocpr  7893  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemfl  7966  ltexprlemfu  7968  aptiprleml  7996  caucvgprprlemexbt  8063  addsrmo  8100  mulsrmo  8101  prodge0  9174  un0addcl  9575  un0mulcl  9576  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  monoord  10900  seq3split  10903  seqsplitg  10904  seqf1oglem1  10934  seq3id2  10941  seqhomog  10945  expnegzap  10988  expcanlem  11131  bcval5  11179  hashfibc  11261  seq3coll  11272  wrdind  11472  wrd2ind  11473  caucvgrelemcau  11724  cau3lem  11858  reccn2ap  12057  summodclem2  12127  zsumdc  12129  fsumf1o  12135  fisumss  12137  fsumcl2lem  12143  fsumadd  12151  fisum0diag2  12192  fsummulc2  12193  mertenslem2  12281  prodmodclem2  12322  zproddc  12324  fprodseq  12328  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodmul  12336  dvds0lem  12546  dvdsnegb  12553  dvdssub2  12580  isprm6  12903  hashgcdeq  12996  modprminv  13006  modprminveq  13007  reumodprminv  13010  pcqmul  13060  pcqcl  13063  pcxnn0cl  13067  pcxcl  13068  pc2dvds  13087  pcadd  13097  pcmpt  13100  pockthg  13114  infpnlem1  13116  ballotfilemfc0  13210  ballotfilemfcc  13211  mgmidsssn0  13681  mhmeql  13776  grprcan  13819  dfgrp3mlem  13880  mulgnn0ass  13938  isnsg3  13987  ghmpreima  14046  ghmeql  14047  lss1d  14692  znidomb  14965  topssnei  15186  innei  15187  cnptopco  15246  cncnpi  15252  cncnp  15254  cnconst2  15257  cnpdis  15266  lmtopcnp  15274  tx2cn  15294  txdis  15301  blssps  15451  blss  15452  neibl  15515  metss  15518  metequiv2  15520  metrest  15530  metcnp3  15535  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemloc  15665  plycolemc  15782  mpodvdsmulf1o  16018  perfectlem2  16028  2sqlem5  16152  2sqlem6  16153  2sqlem8  16156  2sqlem10  16158  nconstwlpolem  17020