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  4370  opelopabt  4404  tpexg  4590  3optocl  4853  fun2ssres  5421  funssfv  5721  fvun1  5769  foco2  5959  f1elima  5979  eloprabga  6175  caovimo  6283  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  brtposg  6525  rdgexggg  6648  rdgivallem  6652  nnmass  6760  nndir  6763  nnaword  6784  th3q  6914  ecovass  6918  ecoviass  6919  fpmg  6955  findcard  7192  unfiin  7233  pr1or2  7540  addasspig  7697  mulasspig  7699  mulcanpig  7702  ltapig  7705  ltmpig  7706  addassnqg  7749  ltbtwnnqq  7782  mulnnnq0  7817  addassnq0  7829  genpassl  7891  genpassu  7892  genpassg  7893  aptiprleml  8006  adddir  8317  le2tri3i  8435  addsub12  8540  subdir  8714  reapmul1  8925  recexaplem2  8982  div12ap  9026  divdiv32ap  9052  divdivap1  9055  lble  9279  zaddcllemneg  9687  fnn0ind  9766  xrltso  10208  iccgelb  10344  elicc4  10352  elfz  10427  fzrevral  10522  expnegap0  10997  expgt0  11022  expge0  11025  expge1  11026  mulexpzap  11029  expp1zap  11038  expm1ap  11039  apexp1  11170  ccatsymb  11384  abssubap0  11871  binom  12267  dvds0lem  12584  dvdsnegb  12591  muldvds1  12599  muldvds2  12600  divalgmodcl  12711  gcd2n0cl  12762  lcmdvds  12873  prmdvdsexp  12943  rpexp1i  12949  eqglact  14077  lss0cl  14755  cnpval  15348  cnf2  15355  cnnei  15382  blssec  15588  blpnfctr  15589  mopni2  15633  mopni3  15634  dvply1  15915  uhgrm  16417  upgrm  16439  upgr1or2  16440