Theorem 3expib 836

Description: Exportation from triple conjunction.

Hypothesis

Ref	Expression
3exp.1	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
3expib	|- (ph -> ((ps /\ ch) -> th))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 832	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp3a 361	1 |- (ph -> ((ps /\ ch) -> th))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  vtocl3ga 1854  3ecoptocl 4305  fodomfibOLD 4567  ser1add2 6338  icoshft 6408  iserzmulc1 7136  mulc1cncf 7279  ivthlem6 7286  ivthlem7 7287  mettri4 7814  opnin 7869  opntop 7870  tgbl 7871  blbas 7872  grpdivf 8085  ghgrpi 8137  ipf 8366  sspival 8397  spwmo 8656  spwval 8659  pilem1 8671  sincosq1sgn 8704  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  efifolem4 8725  efifolem5 8726  shintcl 9293  adjadjt 9860  unopadj2t 9862  hmopadjt 9863  ghomf1olem 10396  homcard 10539  qusp 10555  neifil 10568  filintf 10569  mrdmcd 10722  cmpassoh 10729  homgrf 10730  imonclem 10741  ismonc 10742  cmpmon 10743  icmpmon 10744  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain