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  2836  rspc2ev  2892  reuss  3454  trssord  4428  funtp  5328  resdif  5546  funimass4  5631  fnovex  5979  fnotovb  5990  fovcdm  6091  fnovrn  6096  fmpoco  6304  nndi  6574  nnaordi  6596  ecovass  6733  ecoviass  6734  ecovdi  6735  ecovidi  6736  eqsupti  7100  addasspig  7445  mulasspig  7447  distrpig  7448  distrnq0  7574  addassnq0  7577  distnq0r  7578  prcdnql  7599  prcunqu  7600  genpassl  7639  genpassu  7640  genpassg  7641  distrlem1prl  7697  distrlem1pru  7698  ltexprlemopl  7716  ltexprlemopu  7718  le2tri3i  8183  cnegexlem1  8249  subadd  8277  addsub  8285  subdi  8459  submul2  8473  div12ap  8769  diveqap1  8780  divnegap  8781  divdivap2  8799  ltmulgt11  8939  gt0div  8945  ge0div  8946  uzind3  9488  fnn0ind  9491  qdivcl  9766  irrmul  9770  xrlttr  9919  fzen  10167  ccatval21sw  11064  lswccatn0lsw  11070  swrdwrdsymbg  11120  ccatpfx  11155  lenegsq  11439  moddvds  12143  dvds2add  12169  dvds2sub  12170  dvdsleabs  12189  divalgb  12269  ndvdsadd  12275  modgcd  12345  absmulgcd  12371  odzval  12597  pcmul  12657  setsresg  12903  prdssgrpd  13280  issubmnd  13307  prdsmndd  13313  submcl  13344  grpinvid1  13417  grpinvid2  13418  mulgp1  13524  ghmlin  13617  ghmsub  13620  cmncom  13671  islss3  14174  unopn  14510  innei  14668  cncfi  15083