Theorem 3impa 1177

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 362	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1176	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3impdir  1273  syl3an9b  1289  biimp3a  1324  stoic3  1408  rspec3  2525  rspc3v  2809  raltpg  3584  rextpg  3585  disjiun  3932  otexg  4160  opelopabt  4192  tpexg  4373  3optocl  4625  fun2ssres  5174  funssfv  5455  fvun1  5495  foco2  5663  f1elima  5682  eloprabga  5866  caovimo  5972  ot1stg  6058  ot2ndg  6059  ot3rdgg  6060  brtposg  6159  rdgexggg  6282  rdgivallem  6286  nnmass  6391  nndir  6394  nnaword  6415  th3q  6542  ecovass  6546  ecoviass  6547  fpmg  6576  findcard  6790  unfiin  6822  addasspig  7162  mulasspig  7164  mulcanpig  7167  ltapig  7170  ltmpig  7171  addassnqg  7214  ltbtwnnqq  7247  mulnnnq0  7282  addassnq0  7294  genpassl  7356  genpassu  7357  genpassg  7358  aptiprleml  7471  adddir  7781  le2tri3i  7896  addsub12  7999  subdir  8172  reapmul1  8381  recexaplem2  8437  div12ap  8478  divdiv32ap  8504  divdivap1  8507  lble  8729  zaddcllemneg  9117  fnn0ind  9191  xrltso  9612  iccgelb  9745  elicc4  9753  elfz  9827  fzrevral  9916  expnegap0  10332  expgt0  10357  expge0  10360  expge1  10361  mulexpzap  10364  expp1zap  10373  expm1ap  10374  apexp1  10496  abssubap0  10894  binom  11285  dvds0lem  11539  dvdsnegb  11546  muldvds1  11554  muldvds2  11555  divalgmodcl  11661  gcd2n0cl  11694  lcmdvds  11796  prmdvdsexp  11862  rpexp1i  11868  cnpval  12406  cnf2  12413  cnnei  12440  blssec  12646  blpnfctr  12647  mopni2  12691  mopni3  12692