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 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  animpimp2impd  565  reximddv  2653  rexlimdvaa  2669  issod  4466  ordsuc  4712  fcof1  5992  riota5f  6068  ovmpodf  6223  suppssdc  6504  tfrlemi1  6607  eqsuptid  7343  eqinftid  7367  ordiso2  7381  addnq0mo  7820  mulnq0mo  7821  genprndl  7894  genprndu  7895  addlocpr  7909  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemfl  7982  ltexprlemfu  7984  aptiprleml  8012  caucvgprprlemexbt  8079  addsrmo  8116  mulsrmo  8117  prodge0  9192  un0addcl  9607  un0mulcl  9608  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seqf1oglem1  10977  seq3id2  10984  seqhomog  10988  expnegzap  11031  expcanlem  11175  bcval5  11223  hashfibc  11305  seq3coll  11316  wrdind  11516  wrd2ind  11517  caucvgrelemcau  11768  cau3lem  11903  reccn2ap  12104  summodclem2  12174  zsumdc  12176  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fisum0diag2  12239  fsummulc2  12240  mertenslem2  12328  prodmodclem2  12369  zproddc  12371  fprodseq  12375  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodmul  12383  dvds0lem  12593  dvdsnegb  12600  dvdssub2  12627  isprm6  12951  hashgcdeq  13047  modprminv  13057  modprminveq  13058  reumodprminv  13061  pcqmul  13111  pcqcl  13114  pcxnn0cl  13118  pcxcl  13119  pc2dvds  13138  pcadd  13148  pcmpt  13151  pockthg  13165  infpnlem1  13167  ballotfilemfc0  13290  ballotfilemfcc  13291  mgmidsssn0  13763  mhmeql  13858  grprcan  13901  dfgrp3mlem  13962  mulgnn0ass  14020  isnsg3  14069  ghmpreima  14128  ghmeql  14129  lss1d  14829  znidomb  15102  rnasclassa  15147  topssnei  15388  innei  15389  cnptopco  15448  cncnpi  15454  cncnp  15456  cnconst2  15459  cnpdis  15468  lmtopcnp  15476  tx2cn  15496  txdis  15503  blssps  15653  blss  15654  neibl  15717  metss  15720  metequiv2  15722  metrest  15732  metcnp3  15737  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  plycolemc  15984  rpcxpmul2z  16148  ppinprm  16260  chtnprm  16262  mpodvdsmulf1o  16284  chtublem  16295  perfectlem2  16300  bposlem1  16311  bposlem3  16313  2sqlem5  16443  2sqlem6  16444  2sqlem8  16447  2sqlem10  16449  nconstwlpolem  17322