Theorem 3impa 1221

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

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

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 1007

This theorem is referenced by:  ex3  1222  3impdir  1331  syl3an9b  1347  biimp3a  1382  stoic3  1476  rspec3  2634  rspc3v  2940  raltpg  3747  rextpg  3748  disjiun  4109  otexg  4351  opelopabt  4385  tpexg  4570  3optocl  4833  fun2ssres  5401  funssfv  5701  fvun1  5748  foco2  5932  f1elima  5952  eloprabga  6148  caovimo  6256  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  brtposg  6498  rdgexggg  6621  rdgivallem  6625  nnmass  6733  nndir  6736  nnaword  6757  th3q  6887  ecovass  6891  ecoviass  6892  fpmg  6921  findcard  7158  unfiin  7199  pr1or2  7504  addasspig  7661  mulasspig  7663  mulcanpig  7666  ltapig  7669  ltmpig  7670  addassnqg  7713  ltbtwnnqq  7746  mulnnnq0  7781  addassnq0  7793  genpassl  7855  genpassu  7856  genpassg  7857  aptiprleml  7970  adddir  8281  le2tri3i  8398  addsub12  8502  subdir  8676  reapmul1  8886  recexaplem2  8943  div12ap  8985  divdiv32ap  9011  divdivap1  9014  lble  9238  zaddcllemneg  9633  fnn0ind  9712  xrltso  10148  iccgelb  10284  elicc4  10292  elfz  10367  fzrevral  10461  expnegap0  10933  expgt0  10958  expge0  10961  expge1  10962  mulexpzap  10965  expp1zap  10974  expm1ap  10975  apexp1  11105  ccatsymb  11315  abssubap0  11800  binom  12195  dvds0lem  12512  dvdsnegb  12519  muldvds1  12527  muldvds2  12528  divalgmodcl  12639  gcd2n0cl  12690  lcmdvds  12801  prmdvdsexp  12870  rpexp1i  12876  eqglact  13978  lss0cl  14643  cnpval  15189  cnf2  15196  cnnei  15223  blssec  15429  blpnfctr  15430  mopni2  15474  mopni3  15475  dvply1  15756  uhgrm  16199  upgrm  16221  upgr1or2  16222