Theorem 3expib 835

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 831	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp3a 361	1 |- (ph -> ((ps /\ ch) -> th))

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

This theorem is referenced by:  vtocl3ga 1850  3ecoptocl 4295  fodomfib 4547  ser1add2 6283  icoshft 6349  iserzmulc1 7080  mulc1cncf 7222  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  mettri4 7764  opnin 7821  opntop 7822  tgbl 7823  blbas 7824  grpdivf 8035  ghgrpi 8089  ipf 8313  sspival 8344  spwmo 8598  spwval 8600  pilem1 8609  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  efifolem4 8659  efifolem5 8660  shintcl 9231  adjadjt 9799  unopadj2t 9801  hmopadjt 9802  ghomf1olem 10330  homcard 10462  qusp 10466  neifil 10478  filintf 10479  mrdmcd 10602  cmpassoh 10609  homgrf 10610  imonclem 10619  ismonc 10620  cmpmon 10621  icmpmon 10623

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 776

Copyright terms: Public domain