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  2633  rexlimdvaa  2649  issod  4410  ordsuc  4655  fcof1  5913  riota5f  5987  ovmpodf  6142  tfrlemi1  6484  eqsuptid  7175  eqinftid  7199  ordiso2  7213  addnq0mo  7645  mulnq0mo  7646  genprndl  7719  genprndu  7720  addlocpr  7734  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemfl  7807  ltexprlemfu  7809  aptiprleml  7837  caucvgprprlemexbt  7904  addsrmo  7941  mulsrmo  7942  prodge0  9012  un0addcl  9413  un0mulcl  9414  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  seqf1oglem1  10753  seq3id2  10760  seqhomog  10764  expnegzap  10807  expcanlem  10949  bcval5  10997  seq3coll  11077  wrdind  11269  wrd2ind  11270  caucvgrelemcau  11506  cau3lem  11640  reccn2ap  11839  summodclem2  11908  zsumdc  11910  fsumf1o  11916  fisumss  11918  fsumcl2lem  11924  fsumadd  11932  fisum0diag2  11973  fsummulc2  11974  mertenslem2  12062  prodmodclem2  12103  zproddc  12105  fprodseq  12109  fprodf1o  12114  prodssdc  12115  fprodssdc  12116  fprodmul  12117  dvds0lem  12327  dvdsnegb  12334  dvdssub2  12361  isprm6  12684  hashgcdeq  12777  modprminv  12787  modprminveq  12788  reumodprminv  12791  pcqmul  12841  pcqcl  12844  pcxnn0cl  12848  pcxcl  12849  pc2dvds  12868  pcadd  12878  pcmpt  12881  pockthg  12895  infpnlem1  12897  mgmidsssn0  13432  mhmeql  13540  grprcan  13585  dfgrp3mlem  13646  mulgnn0ass  13710  isnsg3  13759  ghmpreima  13818  ghmeql  13819  lss1d  14362  znidomb  14637  topssnei  14851  innei  14852  cnptopco  14911  cncnpi  14917  cncnp  14919  cnconst2  14922  cnpdis  14931  lmtopcnp  14939  tx2cn  14959  txdis  14966  blssps  15116  blss  15117  neibl  15180  metss  15183  metequiv2  15185  metrest  15195  metcnp3  15200  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemloc  15330  plycolemc  15447  mpodvdsmulf1o  15679  perfectlem2  15689  2sqlem5  15813  2sqlem6  15814  2sqlem8  15817  2sqlem10  15819  nconstwlpolem  16493