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  4464  ordsuc  4710  fcof1  5989  riota5f  6065  ovmpodf  6220  suppssdc  6500  tfrlemi1  6603  eqsuptid  7337  eqinftid  7361  ordiso2  7375  addnq0mo  7814  mulnq0mo  7815  genprndl  7888  genprndu  7889  addlocpr  7903  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemfu  7978  aptiprleml  8006  caucvgprprlemexbt  8073  addsrmo  8110  mulsrmo  8111  prodge0  9184  un0addcl  9596  un0mulcl  9597  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord  10922  seq3split  10925  seqsplitg  10926  seqf1oglem1  10956  seq3id2  10963  seqhomog  10967  expnegzap  11010  expcanlem  11153  bcval5  11201  hashfibc  11283  seq3coll  11294  wrdind  11494  wrd2ind  11495  caucvgrelemcau  11746  cau3lem  11880  reccn2ap  12079  summodclem2  12149  zsumdc  12151  fsumf1o  12157  fisumss  12159  fsumcl2lem  12165  fsumadd  12173  fisum0diag2  12214  fsummulc2  12215  mertenslem2  12303  prodmodclem2  12344  zproddc  12346  fprodseq  12350  fprodf1o  12355  prodssdc  12356  fprodssdc  12357  fprodmul  12358  dvds0lem  12568  dvdsnegb  12575  dvdssub2  12602  isprm6  12925  hashgcdeq  13018  modprminv  13028  modprminveq  13029  reumodprminv  13032  pcqmul  13082  pcqcl  13085  pcxnn0cl  13089  pcxcl  13090  pc2dvds  13109  pcadd  13119  pcmpt  13122  pockthg  13136  infpnlem1  13138  ballotfilemfc0  13232  ballotfilemfcc  13233  mgmidsssn0  13704  mhmeql  13799  grprcan  13842  dfgrp3mlem  13903  mulgnn0ass  13961  isnsg3  14010  ghmpreima  14069  ghmeql  14070  lss1d  14720  znidomb  14993  rnasclassa  15038  topssnei  15263  innei  15264  cnptopco  15323  cncnpi  15329  cncnp  15331  cnconst2  15334  cnpdis  15343  lmtopcnp  15351  tx2cn  15371  txdis  15378  blssps  15528  blss  15529  neibl  15592  metss  15595  metequiv2  15597  metrest  15607  metcnp3  15612  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  plycolemc  15859  mpodvdsmulf1o  16104  perfectlem2  16114  2sqlem5  16238  2sqlem6  16239  2sqlem8  16242  2sqlem10  16244  nconstwlpolem  17115