Theorem 3impa 1221

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

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

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 1007

This theorem is referenced by:  ex3  1222  3impdir  1331  syl3an9b  1347  biimp3a  1382  stoic3  1476  rspec3  2623  rspc3v  2927  raltpg  3726  rextpg  3727  disjiun  4088  otexg  4328  opelopabt  4362  tpexg  4547  3optocl  4810  fun2ssres  5377  funssfv  5674  fvun1  5721  foco2  5904  f1elima  5924  eloprabga  6118  caovimo  6226  ot1stg  6324  ot2ndg  6325  ot3rdgg  6326  brtposg  6463  rdgexggg  6586  rdgivallem  6590  nnmass  6698  nndir  6701  nnaword  6722  th3q  6852  ecovass  6856  ecoviass  6857  fpmg  6886  findcard  7120  unfiin  7161  pr1or2  7459  addasspig  7610  mulasspig  7612  mulcanpig  7615  ltapig  7618  ltmpig  7619  addassnqg  7662  ltbtwnnqq  7695  mulnnnq0  7730  addassnq0  7742  genpassl  7804  genpassu  7805  genpassg  7806  aptiprleml  7919  adddir  8230  le2tri3i  8347  addsub12  8451  subdir  8624  reapmul1  8834  recexaplem2  8891  div12ap  8933  divdiv32ap  8959  divdivap1  8962  lble  9186  zaddcllemneg  9579  fnn0ind  9657  xrltso  10092  iccgelb  10228  elicc4  10236  elfz  10311  fzrevral  10402  expnegap0  10872  expgt0  10897  expge0  10900  expge1  10901  mulexpzap  10904  expp1zap  10913  expm1ap  10914  apexp1  11043  ccatsymb  11245  abssubap0  11730  binom  12125  dvds0lem  12442  dvdsnegb  12449  muldvds1  12457  muldvds2  12458  divalgmodcl  12569  gcd2n0cl  12620  lcmdvds  12731  prmdvdsexp  12800  rpexp1i  12806  eqglact  13892  lss0cl  14465  cnpval  15009  cnf2  15016  cnnei  15043  blssec  15249  blpnfctr  15250  mopni2  15294  mopni3  15295  dvply1  15576  uhgrm  16019  upgrm  16041  upgr1or2  16042