Theorem 3impa 1220

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

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

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 1006

This theorem is referenced by:  ex3  1221  3impdir  1330  syl3an9b  1346  biimp3a  1381  stoic3  1475  rspec3  2622  rspc3v  2926  raltpg  3722  rextpg  3723  disjiun  4083  otexg  4322  opelopabt  4356  tpexg  4541  3optocl  4804  fun2ssres  5370  funssfv  5665  fvun1  5712  foco2  5894  f1elima  5914  eloprabga  6108  caovimo  6216  ot1stg  6315  ot2ndg  6316  ot3rdgg  6317  brtposg  6420  rdgexggg  6543  rdgivallem  6547  nnmass  6655  nndir  6658  nnaword  6679  th3q  6809  ecovass  6813  ecoviass  6814  fpmg  6843  findcard  7077  unfiin  7118  pr1or2  7399  addasspig  7550  mulasspig  7552  mulcanpig  7555  ltapig  7558  ltmpig  7559  addassnqg  7602  ltbtwnnqq  7635  mulnnnq0  7670  addassnq0  7682  genpassl  7744  genpassu  7745  genpassg  7746  aptiprleml  7859  adddir  8170  le2tri3i  8288  addsub12  8392  subdir  8565  reapmul1  8775  recexaplem2  8832  div12ap  8874  divdiv32ap  8900  divdivap1  8903  lble  9127  zaddcllemneg  9518  fnn0ind  9596  xrltso  10031  iccgelb  10167  elicc4  10175  elfz  10249  fzrevral  10340  expnegap0  10809  expgt0  10834  expge0  10837  expge1  10838  mulexpzap  10841  expp1zap  10850  expm1ap  10851  apexp1  10980  ccatsymb  11179  abssubap0  11651  binom  12046  dvds0lem  12363  dvdsnegb  12370  muldvds1  12378  muldvds2  12379  divalgmodcl  12490  gcd2n0cl  12541  lcmdvds  12652  prmdvdsexp  12721  rpexp1i  12727  eqglact  13813  lss0cl  14385  cnpval  14924  cnf2  14931  cnnei  14958  blssec  15164  blpnfctr  15165  mopni2  15209  mopni3  15210  dvply1  15491  uhgrm  15931  upgrm  15953  upgr1or2  15954