Theorem 3impb 1230

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

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

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 1011

This theorem is referenced by:  3adant1l  1261  3adant1r  1262  3impdi  1334  vtocl3gf  2886  rspc2ev  2945  reuss  3514  trssord  4520  funtp  5429  resdif  5656  funimass4  5747  fnovex  6108  fnotovb  6121  fovcdm  6222  fnovrn  6227  fmpoco  6442  nndi  6749  nnaordi  6771  ecovass  6908  ecoviass  6909  ecovdi  6910  ecovidi  6911  eqsupti  7326  addasspig  7687  mulasspig  7689  distrpig  7690  distrnq0  7816  addassnq0  7819  distnq0r  7820  prcdnql  7841  prcunqu  7842  genpassl  7881  genpassu  7882  genpassg  7883  distrlem1prl  7939  distrlem1pru  7940  ltexprlemopl  7958  ltexprlemopu  7960  le2tri3i  8424  cnegexlem1  8491  subadd  8519  addsub  8527  subdi  8702  submul2  8716  div12ap  9014  diveqap1  9025  divnegap  9026  divdivap2  9044  ltmulgt11  9184  gt0div  9190  ge0div  9191  uzind3  9738  fnn0ind  9741  qdivcl  10022  irrmul  10026  xrlttr  10176  fzen  10426  ccatval21sw  11351  lswccatn0lsw  11357  swrdwrdsymbg  11414  ccatpfx  11451  ccatopth  11466  lenegsq  11839  moddvds  12544  dvds2add  12570  dvds2sub  12571  dvdsleabs  12590  divalgb  12670  ndvdsadd  12676  modgcd  12746  absmulgcd  12772  odzval  12998  pcmul  13058  setsresg  13368  issubmnd  13732  submcl  13763  grpinvid1  13834  grpinvid2  13835  mulgp1  13935  ghmlin  14028  ghmsub  14031  cmncom  14082  prdssgrpd  14168  prdsmndd  14171  islss3  14688  unopn  15029  innei  15187  cncfi  15602