Theorem 3impa 1197

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 364	. 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:  ex3  1198  3impdir  1307  syl3an9b  1323  biimp3a  1358  stoic3  1451  rspec3  2596  rspc3v  2893  raltpg  3686  rextpg  3687  disjiun  4040  otexg  4275  opelopabt  4309  tpexg  4492  3optocl  4754  fun2ssres  5315  funssfv  5604  fvun1  5647  foco2  5824  f1elima  5844  eloprabga  6034  caovimo  6142  ot1stg  6240  ot2ndg  6241  ot3rdgg  6242  brtposg  6342  rdgexggg  6465  rdgivallem  6469  nnmass  6575  nndir  6578  nnaword  6599  th3q  6729  ecovass  6733  ecoviass  6734  fpmg  6763  findcard  6987  unfiin  7025  addasspig  7445  mulasspig  7447  mulcanpig  7450  ltapig  7453  ltmpig  7454  addassnqg  7497  ltbtwnnqq  7530  mulnnnq0  7565  addassnq0  7577  genpassl  7639  genpassu  7640  genpassg  7641  aptiprleml  7754  adddir  8065  le2tri3i  8183  addsub12  8287  subdir  8460  reapmul1  8670  recexaplem2  8727  div12ap  8769  divdiv32ap  8795  divdivap1  8798  lble  9022  zaddcllemneg  9413  fnn0ind  9491  xrltso  9920  iccgelb  10056  elicc4  10064  elfz  10138  fzrevral  10229  expnegap0  10694  expgt0  10719  expge0  10722  expge1  10723  mulexpzap  10726  expp1zap  10735  expm1ap  10736  apexp1  10865  ccatsymb  11061  abssubap0  11434  binom  11828  dvds0lem  12145  dvdsnegb  12152  muldvds1  12160  muldvds2  12161  divalgmodcl  12272  gcd2n0cl  12323  lcmdvds  12434  prmdvdsexp  12503  rpexp1i  12509  eqglact  13594  lss0cl  14164  cnpval  14703  cnf2  14710  cnnei  14737  blssec  14943  blpnfctr  14944  mopni2  14988  mopni3  14989  dvply1  15270