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  2647  rexlimdvaa  2663  issod  4445  ordsuc  4690  fcof1  5962  riota5f  6038  ovmpodf  6193  suppssdc  6473  tfrlemi1  6576  eqsuptid  7301  eqinftid  7325  ordiso2  7339  addnq0mo  7778  mulnq0mo  7779  genprndl  7852  genprndu  7853  addlocpr  7867  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemfl  7940  ltexprlemfu  7942  aptiprleml  7970  caucvgprprlemexbt  8037  addsrmo  8074  mulsrmo  8075  prodge0  9145  un0addcl  9546  un0mulcl  9547  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  seqf1oglem1  10905  seq3id2  10912  seqhomog  10916  expnegzap  10959  expcanlem  11102  bcval5  11150  hashfibc  11232  seq3coll  11239  wrdind  11439  wrd2ind  11440  caucvgrelemcau  11690  cau3lem  11824  reccn2ap  12023  summodclem2  12093  zsumdc  12095  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  fisum0diag2  12158  fsummulc2  12159  mertenslem2  12247  prodmodclem2  12288  zproddc  12290  fprodseq  12294  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  dvds0lem  12512  dvdsnegb  12519  dvdssub2  12546  isprm6  12869  hashgcdeq  12962  modprminv  12972  modprminveq  12973  reumodprminv  12976  pcqmul  13026  pcqcl  13029  pcxnn0cl  13033  pcxcl  13034  pc2dvds  13053  pcadd  13063  pcmpt  13066  pockthg  13080  infpnlem1  13082  ballotfilemfc0  13176  ballotfilemfcc  13177  mgmidsssn0  13647  mhmeql  13747  grprcan  13792  dfgrp3mlem  13853  mulgnn0ass  13911  isnsg3  13960  ghmpreima  14019  ghmeql  14020  lss1d  14657  znidomb  14932  topssnei  15153  innei  15154  cnptopco  15213  cncnpi  15219  cncnp  15221  cnconst2  15224  cnpdis  15233  lmtopcnp  15241  tx2cn  15261  txdis  15268  blssps  15418  blss  15419  neibl  15482  metss  15485  metequiv2  15487  metrest  15497  metcnp3  15502  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemloc  15632  plycolemc  15749  mpodvdsmulf1o  15984  perfectlem2  15994  2sqlem5  16118  2sqlem6  16119  2sqlem8  16122  2sqlem10  16124  nconstwlpolem  16977