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  10810  expgt0  10835  expge0  10838  expge1  10839  mulexpzap  10842  expp1zap  10851  expm1ap  10852  apexp1  10981  ccatsymb  11183  abssubap0  11668  binom  12063  dvds0lem  12380  dvdsnegb  12387  muldvds1  12395  muldvds2  12396  divalgmodcl  12507  gcd2n0cl  12558  lcmdvds  12669  prmdvdsexp  12738  rpexp1i  12744  eqglact  13830  lss0cl  14402  cnpval  14941  cnf2  14948  cnnei  14975  blssec  15181  blpnfctr  15182  mopni2  15226  mopni3  15227  dvply1  15508  uhgrm  15948  upgrm  15970  upgr1or2  15971