Theorem 3impa 1196

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

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

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 982

This theorem is referenced by:  ex3  1197  3impdir  1305  syl3an9b  1321  biimp3a  1356  stoic3  1442  rspec3  2587  rspc3v  2884  raltpg  3675  rextpg  3676  disjiun  4028  otexg  4263  opelopabt  4296  tpexg  4479  3optocl  4741  fun2ssres  5301  funssfv  5584  fvun1  5627  foco2  5800  f1elima  5820  eloprabga  6009  caovimo  6117  ot1stg  6210  ot2ndg  6211  ot3rdgg  6212  brtposg  6312  rdgexggg  6435  rdgivallem  6439  nnmass  6545  nndir  6548  nnaword  6569  th3q  6699  ecovass  6703  ecoviass  6704  fpmg  6733  findcard  6949  unfiin  6987  addasspig  7397  mulasspig  7399  mulcanpig  7402  ltapig  7405  ltmpig  7406  addassnqg  7449  ltbtwnnqq  7482  mulnnnq0  7517  addassnq0  7529  genpassl  7591  genpassu  7592  genpassg  7593  aptiprleml  7706  adddir  8017  le2tri3i  8135  addsub12  8239  subdir  8412  reapmul1  8622  recexaplem2  8679  div12ap  8721  divdiv32ap  8747  divdivap1  8750  lble  8974  zaddcllemneg  9365  fnn0ind  9442  xrltso  9871  iccgelb  10007  elicc4  10015  elfz  10089  fzrevral  10180  expnegap0  10639  expgt0  10664  expge0  10667  expge1  10668  mulexpzap  10671  expp1zap  10680  expm1ap  10681  apexp1  10810  abssubap0  11255  binom  11649  dvds0lem  11966  dvdsnegb  11973  muldvds1  11981  muldvds2  11982  divalgmodcl  12093  gcd2n0cl  12136  lcmdvds  12247  prmdvdsexp  12316  rpexp1i  12322  eqglact  13355  lss0cl  13925  cnpval  14434  cnf2  14441  cnnei  14468  blssec  14674  blpnfctr  14675  mopni2  14719  mopni3  14720  dvply1  15001