Theorem 3impb 1202

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	exp32 365	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1196	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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 depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  3adant1l  1233  3adant1r  1234  3impdi  1306  vtocl3gf  2841  rspc2ev  2899  reuss  3462  trssord  4445  funtp  5346  resdif  5566  funimass4  5652  fnovex  6000  fnotovb  6011  fovcdm  6112  fnovrn  6117  fmpoco  6325  nndi  6595  nnaordi  6617  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  eqsupti  7124  addasspig  7478  mulasspig  7480  distrpig  7481  distrnq0  7607  addassnq0  7610  distnq0r  7611  prcdnql  7632  prcunqu  7633  genpassl  7672  genpassu  7673  genpassg  7674  distrlem1prl  7730  distrlem1pru  7731  ltexprlemopl  7749  ltexprlemopu  7751  le2tri3i  8216  cnegexlem1  8282  subadd  8310  addsub  8318  subdi  8492  submul2  8506  div12ap  8802  diveqap1  8813  divnegap  8814  divdivap2  8832  ltmulgt11  8972  gt0div  8978  ge0div  8979  uzind3  9521  fnn0ind  9524  qdivcl  9799  irrmul  9803  xrlttr  9952  fzen  10200  ccatval21sw  11099  lswccatn0lsw  11105  swrdwrdsymbg  11155  ccatpfx  11192  ccatopth  11207  lenegsq  11521  moddvds  12225  dvds2add  12251  dvds2sub  12252  dvdsleabs  12271  divalgb  12351  ndvdsadd  12357  modgcd  12427  absmulgcd  12453  odzval  12679  pcmul  12739  setsresg  12985  prdssgrpd  13362  issubmnd  13389  prdsmndd  13395  submcl  13426  grpinvid1  13499  grpinvid2  13500  mulgp1  13606  ghmlin  13699  ghmsub  13702  cmncom  13753  islss3  14256  unopn  14592  innei  14750  cncfi  15165