Theorem 3impa 1225

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ex3  1226  3impdir  1335  syl3an9b  1351  biimp3a  1386  stoic3  1480  rspec3  2640  rspc3v  2946  raltpg  3762  rextpg  3763  disjiun  4125  otexg  4372  opelopabt  4406  tpexg  4592  3optocl  4855  fun2ssres  5424  funssfv  5724  fvun1  5772  foco2  5962  f1elima  5982  eloprabga  6178  caovimo  6286  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  brtposg  6529  rdgexggg  6652  rdgivallem  6656  nnmass  6764  nndir  6767  nnaword  6788  th3q  6918  ecovass  6922  ecoviass  6923  fpmg  6959  findcard  7196  unfiin  7237  pr1or2  7546  addasspig  7703  mulasspig  7705  mulcanpig  7708  ltapig  7711  ltmpig  7712  addassnqg  7755  ltbtwnnqq  7788  mulnnnq0  7823  addassnq0  7835  genpassl  7897  genpassu  7898  genpassg  7899  aptiprleml  8012  adddir  8323  le2tri3i  8441  addsub12  8546  subdir  8720  reapmul1  8931  recexaplem2  8988  div12ap  9032  divdiv32ap  9058  divdivap1  9061  lble  9285  zaddcllemneg  9694  fnn0ind  9773  xrltso  10215  iccgelb  10351  elicc4  10359  elfz  10434  fzrevral  10529  expnegap0  11005  expgt0  11030  expge0  11033  expge1  11034  mulexpzap  11037  expp1zap  11046  expm1ap  11047  apexp1  11178  ccatsymb  11392  abssubap0  11879  binom  12276  dvds0lem  12593  dvdsnegb  12600  muldvds1  12608  muldvds2  12609  divalgmodcl  12720  gcd2n0cl  12771  lcmdvds  12882  prmdvdsexp  12952  rpexp1i  12958  eqglact  14087  lss0cl  14815  cnpval  15424  cnf2  15431  cnnei  15458  blssec  15664  blpnfctr  15665  mopni2  15709  mopni3  15710  dvply1  15991  uhgrm  16524  upgrm  16546  upgr1or2  16547