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  4414  ordsuc  4659  fcof1  5919  riota5f  5993  ovmpodf  6148  tfrlemi1  6493  eqsuptid  7187  eqinftid  7211  ordiso2  7225  addnq0mo  7657  mulnq0mo  7658  genprndl  7731  genprndu  7732  addlocpr  7746  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemfl  7819  ltexprlemfu  7821  aptiprleml  7849  caucvgprprlemexbt  7916  addsrmo  7953  mulsrmo  7954  prodge0  9024  un0addcl  9425  un0mulcl  9426  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  seq3split  10740  seqsplitg  10741  seqf1oglem1  10771  seq3id2  10778  seqhomog  10782  expnegzap  10825  expcanlem  10967  bcval5  11015  seq3coll  11096  wrdind  11293  wrd2ind  11294  caucvgrelemcau  11531  cau3lem  11665  reccn2ap  11864  summodclem2  11933  zsumdc  11935  fsumf1o  11941  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  fisum0diag2  11998  fsummulc2  11999  mertenslem2  12087  prodmodclem2  12128  zproddc  12130  fprodseq  12134  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodmul  12142  dvds0lem  12352  dvdsnegb  12359  dvdssub2  12386  isprm6  12709  hashgcdeq  12802  modprminv  12812  modprminveq  12813  reumodprminv  12816  pcqmul  12866  pcqcl  12869  pcxnn0cl  12873  pcxcl  12874  pc2dvds  12893  pcadd  12903  pcmpt  12906  pockthg  12920  infpnlem1  12922  mgmidsssn0  13457  mhmeql  13565  grprcan  13610  dfgrp3mlem  13671  mulgnn0ass  13735  isnsg3  13784  ghmpreima  13843  ghmeql  13844  lss1d  14387  znidomb  14662  topssnei  14876  innei  14877  cnptopco  14936  cncnpi  14942  cncnp  14944  cnconst2  14947  cnpdis  14956  lmtopcnp  14964  tx2cn  14984  txdis  14991  blssps  15141  blss  15142  neibl  15205  metss  15208  metequiv2  15210  metrest  15220  metcnp3  15225  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  plycolemc  15472  mpodvdsmulf1o  15704  perfectlem2  15714  2sqlem5  15838  2sqlem6  15839  2sqlem8  15842  2sqlem10  15844  nconstwlpolem  16605