Theorem 3expib 848

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

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787

This theorem is referenced by:  vtocl3ga 1901  3ecoptocl 4366  fodomfib 4627  icoshf 6434  ser1add2i 6597  iserzmulc1 7226  mulc1cncf 7369  ivthlem6 7376  ivthlem7 7377  mettri4 7899  opnin 7954  opntop 7955  tgbl 7956  blbas 7957  grpdivf 8169  ghgrpi 8221  ipf 8450  sspival 8481  spwmo 8740  spwval 8743  pilem1 8754  sincosq1sgn 8787  sincosq2sgn 8788  sincosq3sgn 8789  sincosq4sgn 8790  efifolem4 8808  efifolem5 8809  shintcli 9376  adjadj 9943  unopadj2 9945  hmopadj 9946  ghomf1olem 10481  homcard 10633  qusp 10649  neifil 10661  filintf 10662  mrdmcd 10804  cmpassoh 10811  imonclem 10823  ismonc 10824  cmpmon 10825  icmpmon 10826  iepiclem 10833  isepic 10834  idfisf 10844

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 154  df-an 232  df-3an 789

Copyright terms: Public domain