Theorem 3impb 1225

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 1219	1 |- ( ( ph /\ ps /\ ch ) -> th )

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

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 1006

This theorem is referenced by:  3adant1l  1256  3adant1r  1257  3impdi  1329  vtocl3gf  2867  rspc2ev  2925  reuss  3488  trssord  4477  funtp  5383  resdif  5605  funimass4  5696  fnovex  6051  fnotovb  6064  fovcdm  6165  fnovrn  6170  fmpoco  6381  nndi  6654  nnaordi  6676  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  eqsupti  7195  addasspig  7550  mulasspig  7552  distrpig  7553  distrnq0  7679  addassnq0  7682  distnq0r  7683  prcdnql  7704  prcunqu  7705  genpassl  7744  genpassu  7745  genpassg  7746  distrlem1prl  7802  distrlem1pru  7803  ltexprlemopl  7821  ltexprlemopu  7823  le2tri3i  8288  cnegexlem1  8354  subadd  8382  addsub  8390  subdi  8564  submul2  8578  div12ap  8874  diveqap1  8885  divnegap  8886  divdivap2  8904  ltmulgt11  9044  gt0div  9050  ge0div  9051  uzind3  9593  fnn0ind  9596  qdivcl  9877  irrmul  9881  xrlttr  10030  fzen  10278  ccatval21sw  11186  lswccatn0lsw  11192  swrdwrdsymbg  11249  ccatpfx  11286  ccatopth  11301  lenegsq  11673  moddvds  12378  dvds2add  12404  dvds2sub  12405  dvdsleabs  12424  divalgb  12504  ndvdsadd  12510  modgcd  12580  absmulgcd  12606  odzval  12832  pcmul  12892  setsresg  13138  prdssgrpd  13516  issubmnd  13543  prdsmndd  13549  submcl  13580  grpinvid1  13653  grpinvid2  13654  mulgp1  13760  ghmlin  13853  ghmsub  13856  cmncom  13907  islss3  14412  unopn  14748  innei  14906  cncfi  15321