Theorem 3impa 1176

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

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

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 964

This theorem is referenced by:  3impdir  1272  syl3an9b  1288  biimp3a  1323  stoic3  1407  rspec3  2522  rspc3v  2805  raltpg  3576  rextpg  3577  disjiun  3924  otexg  4152  opelopabt  4184  tpexg  4365  3optocl  4617  fun2ssres  5166  funssfv  5447  fvun1  5487  foco2  5655  f1elima  5674  eloprabga  5858  caovimo  5964  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  brtposg  6151  rdgexggg  6274  rdgivallem  6278  nnmass  6383  nndir  6386  nnaword  6407  th3q  6534  ecovass  6538  ecoviass  6539  fpmg  6568  findcard  6782  unfiin  6814  addasspig  7145  mulasspig  7147  mulcanpig  7150  ltapig  7153  ltmpig  7154  addassnqg  7197  ltbtwnnqq  7230  mulnnnq0  7265  addassnq0  7277  genpassl  7339  genpassu  7340  genpassg  7341  aptiprleml  7454  adddir  7764  le2tri3i  7879  addsub12  7982  subdir  8155  reapmul1  8364  recexaplem2  8420  div12ap  8461  divdiv32ap  8487  divdivap1  8490  lble  8712  zaddcllemneg  9100  fnn0ind  9174  xrltso  9589  iccgelb  9722  elicc4  9730  elfz  9803  fzrevral  9892  expnegap0  10308  expgt0  10333  expge0  10336  expge1  10337  mulexpzap  10340  expp1zap  10349  expm1ap  10350  abssubap0  10869  binom  11260  dvds0lem  11510  dvdsnegb  11517  muldvds1  11525  muldvds2  11526  divalgmodcl  11632  gcd2n0cl  11665  lcmdvds  11767  prmdvdsexp  11833  rpexp1i  11839  cnpval  12377  cnf2  12384  cnnei  12411  blssec  12617  blpnfctr  12618  mopni2  12662  mopni3  12663