Theorem 3impa 1133

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

Hypothesis

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

Assertion

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

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	exp31 356	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1132	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3impdir  1225  syl3an9b  1241  biimp3a  1276  stoic3  1360  rspec3  2451  rspc3v  2716  raltpg  3445  rextpg  3446  otexg  3985  opelopabt  4017  tpexg  4197  3optocl  4436  fun2ssres  4963  funssfv  5220  fvun1  5260  foco2  5339  f1elima  5433  eloprabga  5611  caovimo  5714  ot1stg  5799  ot2ndg  5800  ot3rdgg  5801  brtposg  5892  rdgexggg  5987  rdgivallem  5991  frecsuclem1  6010  nnmass  6089  nndir  6092  nnaword  6107  th3q  6234  ecovass  6238  ecoviass  6239  findcard  6372  addasspig  6520  mulasspig  6522  mulcanpig  6525  ltapig  6528  ltmpig  6529  addassnqg  6572  ltbtwnnqq  6605  mulnnnq0  6640  addassnq0  6652  genpassl  6714  genpassu  6715  genpassg  6716  aptiprleml  6829  adddir  7110  le2tri3i  7219  addsub12  7321  subdir  7490  reapmul1  7695  recexaplem2  7742  div12ap  7782  divdiv32ap  7808  divdivap1  7811  lble  8025  zaddcllemneg  8390  fnn0ind  8463  xrltso  8871  iccgelb  8955  elicc4  8963  elfz  9035  fzrevral  9122  expivallem  9477  expnegap0  9484  expgt0  9509  expge0  9512  expge1  9513  mulexpzap  9516  expp1zap  9525  expm1ap  9526  abssubap0  9976  dvds0lem  10205  dvdsnegb  10212  muldvds1  10220  muldvds2  10221  divalgmodcl  10328  gcd2n0cl  10361  lcmdvds  10461  prmdvdsexp  10527  rpexp1i  10533