Theorem 3impa 1218

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

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

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 1004

This theorem is referenced by:  ex3  1219  3impdir  1328  syl3an9b  1344  biimp3a  1379  stoic3  1473  rspec3  2620  rspc3v  2923  raltpg  3719  rextpg  3720  disjiun  4078  otexg  4316  opelopabt  4350  tpexg  4535  3optocl  4797  fun2ssres  5361  funssfv  5655  fvun1  5702  foco2  5883  f1elima  5903  eloprabga  6097  caovimo  6205  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  brtposg  6406  rdgexggg  6529  rdgivallem  6533  nnmass  6641  nndir  6644  nnaword  6665  th3q  6795  ecovass  6799  ecoviass  6800  fpmg  6829  findcard  7058  unfiin  7099  pr1or2  7378  addasspig  7528  mulasspig  7530  mulcanpig  7533  ltapig  7536  ltmpig  7537  addassnqg  7580  ltbtwnnqq  7613  mulnnnq0  7648  addassnq0  7660  genpassl  7722  genpassu  7723  genpassg  7724  aptiprleml  7837  adddir  8148  le2tri3i  8266  addsub12  8370  subdir  8543  reapmul1  8753  recexaplem2  8810  div12ap  8852  divdiv32ap  8878  divdivap1  8881  lble  9105  zaddcllemneg  9496  fnn0ind  9574  xrltso  10004  iccgelb  10140  elicc4  10148  elfz  10222  fzrevral  10313  expnegap0  10781  expgt0  10806  expge0  10809  expge1  10810  mulexpzap  10813  expp1zap  10822  expm1ap  10823  apexp1  10952  ccatsymb  11150  abssubap0  11617  binom  12011  dvds0lem  12328  dvdsnegb  12335  muldvds1  12343  muldvds2  12344  divalgmodcl  12455  gcd2n0cl  12506  lcmdvds  12617  prmdvdsexp  12686  rpexp1i  12692  eqglact  13778  lss0cl  14349  cnpval  14888  cnf2  14895  cnnei  14922  blssec  15128  blpnfctr  15129  mopni2  15173  mopni3  15174  dvply1  15455  uhgrm  15894  upgrm  15916  upgr1or2  15917