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  2593  rexlimdvaa  2608  issod  4344  ordsuc  4587  fcof1  5814  riota5f  5886  ovmpodf  6038  tfrlemi1  6372  eqsuptid  7042  eqinftid  7066  ordiso2  7080  addnq0mo  7493  mulnq0mo  7494  genprndl  7567  genprndu  7568  addlocpr  7582  ltexprlemm  7646  ltexprlemopl  7647  ltexprlemopu  7649  ltexprlemfl  7655  ltexprlemfu  7657  aptiprleml  7685  caucvgprprlemexbt  7752  addsrmo  7789  mulsrmo  7790  prodge0  8859  un0addcl  9259  un0mulcl  9260  seq3fveq2  10531  seq3shft2  10535  monoord  10538  seq3split  10541  seq3id2  10571  seqhomog  10575  expnegzap  10618  expcanlem  10760  bcval5  10808  seq3coll  10887  caucvgrelemcau  11098  cau3lem  11232  reccn2ap  11430  summodclem2  11499  zsumdc  11501  fsumf1o  11507  fisumss  11509  fsumcl2lem  11515  fsumadd  11523  fisum0diag2  11564  fsummulc2  11565  mertenslem2  11653  prodmodclem2  11694  zproddc  11696  fprodseq  11700  fprodf1o  11705  prodssdc  11706  fprodssdc  11707  fprodmul  11708  dvds0lem  11918  dvdsnegb  11925  dvdssub2  11952  isprm6  12259  hashgcdeq  12351  modprminv  12361  modprminveq  12362  reumodprminv  12365  pcqmul  12415  pcqcl  12418  pcxnn0cl  12422  pcxcl  12423  pc2dvds  12442  pcadd  12452  pcmpt  12455  pockthg  12469  infpnlem1  12471  mgmidsssn0  12941  mhmeql  13038  grprcan  13083  dfgrp3mlem  13144  mulgnn0ass  13202  isnsg3  13250  ghmpreima  13309  ghmeql  13310  lss1d  13843  znidomb  14103  topssnei  14287  innei  14288  cnptopco  14347  cncnpi  14353  cncnp  14355  cnconst2  14358  cnpdis  14367  lmtopcnp  14375  tx2cn  14395  txdis  14402  blssps  14552  blss  14553  neibl  14616  metss  14619  metequiv2  14621  metrest  14631  metcnp3  14636  ivthinclemlopn  14747  ivthinclemlr  14748  ivthinclemuopn  14749  ivthinclemur  14750  ivthinclemloc  14752  2sqlem5  15130  2sqlem6  15131  2sqlem8  15134  2sqlem10  15136  nconstwlpolem  15479