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  3676  rextpg  3677  disjiun  4029  otexg  4264  opelopabt  4297  tpexg  4480  3optocl  4742  fun2ssres  5302  funssfv  5587  fvun1  5630  foco2  5803  f1elima  5823  eloprabga  6013  caovimo  6121  ot1stg  6219  ot2ndg  6220  ot3rdgg  6221  brtposg  6321  rdgexggg  6444  rdgivallem  6448  nnmass  6554  nndir  6557  nnaword  6578  th3q  6708  ecovass  6712  ecoviass  6713  fpmg  6742  findcard  6958  unfiin  6996  addasspig  7414  mulasspig  7416  mulcanpig  7419  ltapig  7422  ltmpig  7423  addassnqg  7466  ltbtwnnqq  7499  mulnnnq0  7534  addassnq0  7546  genpassl  7608  genpassu  7609  genpassg  7610  aptiprleml  7723  adddir  8034  le2tri3i  8152  addsub12  8256  subdir  8429  reapmul1  8639  recexaplem2  8696  div12ap  8738  divdiv32ap  8764  divdivap1  8767  lble  8991  zaddcllemneg  9382  fnn0ind  9459  xrltso  9888  iccgelb  10024  elicc4  10032  elfz  10106  fzrevral  10197  expnegap0  10656  expgt0  10681  expge0  10684  expge1  10685  mulexpzap  10688  expp1zap  10697  expm1ap  10698  apexp1  10827  abssubap0  11272  binom  11666  dvds0lem  11983  dvdsnegb  11990  muldvds1  11998  muldvds2  11999  divalgmodcl  12110  gcd2n0cl  12161  lcmdvds  12272  prmdvdsexp  12341  rpexp1i  12347  eqglact  13431  lss0cl  14001  cnpval  14518  cnf2  14525  cnnei  14552  blssec  14758  blpnfctr  14759  mopni2  14803  mopni3  14804  dvply1  15085