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  4337  ordsuc  4580  fcof1  5805  riota5f  5877  ovmpodf  6029  tfrlemi1  6358  eqsuptid  7027  eqinftid  7051  ordiso2  7065  addnq0mo  7477  mulnq0mo  7478  genprndl  7551  genprndu  7552  addlocpr  7566  ltexprlemm  7630  ltexprlemopl  7631  ltexprlemopu  7633  ltexprlemfl  7639  ltexprlemfu  7641  aptiprleml  7669  caucvgprprlemexbt  7736  addsrmo  7773  mulsrmo  7774  prodge0  8842  un0addcl  9240  un0mulcl  9241  seq3fveq2  10502  seq3shft2  10506  monoord  10509  seq3split  10512  seq3id2  10542  expnegzap  10588  expcanlem  10730  bcval5  10778  seq3coll  10857  caucvgrelemcau  11024  cau3lem  11158  reccn2ap  11356  summodclem2  11425  zsumdc  11427  fsumf1o  11433  fisumss  11435  fsumcl2lem  11441  fsumadd  11449  fisum0diag2  11490  fsummulc2  11491  mertenslem2  11579  prodmodclem2  11620  zproddc  11622  fprodseq  11626  fprodf1o  11631  prodssdc  11632  fprodssdc  11633  fprodmul  11634  dvds0lem  11843  dvdsnegb  11850  dvdssub2  11877  isprm6  12182  hashgcdeq  12274  modprminv  12284  modprminveq  12285  reumodprminv  12288  pcqmul  12338  pcqcl  12341  pcxnn0cl  12345  pcxcl  12346  pc2dvds  12365  pcadd  12375  pcmpt  12378  pockthg  12392  infpnlem1  12394  mgmidsssn0  12863  mhmeql  12959  grprcan  12996  dfgrp3mlem  13057  mulgnn0ass  13115  isnsg3  13163  ghmpreima  13222  ghmeql  13223  lss1d  13716  topssnei  14139  innei  14140  cnptopco  14199  cncnpi  14205  cncnp  14207  cnconst2  14210  cnpdis  14219  lmtopcnp  14227  tx2cn  14247  txdis  14254  blssps  14404  blss  14405  neibl  14468  metss  14471  metequiv2  14473  metrest  14483  metcnp3  14488  ivthinclemlopn  14591  ivthinclemlr  14592  ivthinclemuopn  14593  ivthinclemur  14594  ivthinclemloc  14596  2sqlem5  14944  2sqlem6  14945  2sqlem8  14948  2sqlem10  14950  nconstwlpolem  15292