Theorem 3impa 1195

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 1194	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 979

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 981

This theorem is referenced by:  ex3  1196  3impdir  1304  syl3an9b  1320  biimp3a  1355  stoic3  1441  rspec3  2577  rspc3v  2869  raltpg  3657  rextpg  3658  disjiun  4010  otexg  4242  opelopabt  4274  tpexg  4456  3optocl  4716  fun2ssres  5271  funssfv  5553  fvun1  5595  foco2  5767  f1elima  5787  eloprabga  5975  caovimo  6082  ot1stg  6167  ot2ndg  6168  ot3rdgg  6169  brtposg  6269  rdgexggg  6392  rdgivallem  6396  nnmass  6502  nndir  6505  nnaword  6526  th3q  6654  ecovass  6658  ecoviass  6659  fpmg  6688  findcard  6902  unfiin  6939  addasspig  7343  mulasspig  7345  mulcanpig  7348  ltapig  7351  ltmpig  7352  addassnqg  7395  ltbtwnnqq  7428  mulnnnq0  7463  addassnq0  7475  genpassl  7537  genpassu  7538  genpassg  7539  aptiprleml  7652  adddir  7962  le2tri3i  8080  addsub12  8184  subdir  8357  reapmul1  8566  recexaplem2  8623  div12ap  8665  divdiv32ap  8691  divdivap1  8694  lble  8918  zaddcllemneg  9306  fnn0ind  9383  xrltso  9810  iccgelb  9946  elicc4  9954  elfz  10028  fzrevral  10119  expnegap0  10542  expgt0  10567  expge0  10570  expge1  10571  mulexpzap  10574  expp1zap  10583  expm1ap  10584  apexp1  10712  abssubap0  11113  binom  11506  dvds0lem  11822  dvdsnegb  11829  muldvds1  11837  muldvds2  11838  divalgmodcl  11947  gcd2n0cl  11984  lcmdvds  12093  prmdvdsexp  12162  rpexp1i  12168  eqglact  13117  lss0cl  13558  cnpval  13994  cnf2  14001  cnnei  14028  blssec  14234  blpnfctr  14235  mopni2  14279  mopni3  14280