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  5653  fvun1  5700  foco2  5877  f1elima  5897  eloprabga  6091  caovimo  6199  ot1stg  6298  ot2ndg  6299  ot3rdgg  6300  brtposg  6400  rdgexggg  6523  rdgivallem  6527  nnmass  6633  nndir  6636  nnaword  6657  th3q  6787  ecovass  6791  ecoviass  6792  fpmg  6821  findcard  7050  unfiin  7088  pr1or2  7367  addasspig  7517  mulasspig  7519  mulcanpig  7522  ltapig  7525  ltmpig  7526  addassnqg  7569  ltbtwnnqq  7602  mulnnnq0  7637  addassnq0  7649  genpassl  7711  genpassu  7712  genpassg  7713  aptiprleml  7826  adddir  8137  le2tri3i  8255  addsub12  8359  subdir  8532  reapmul1  8742  recexaplem2  8799  div12ap  8841  divdiv32ap  8867  divdivap1  8870  lble  9094  zaddcllemneg  9485  fnn0ind  9563  xrltso  9992  iccgelb  10128  elicc4  10136  elfz  10210  fzrevral  10301  expnegap0  10769  expgt0  10794  expge0  10797  expge1  10798  mulexpzap  10801  expp1zap  10810  expm1ap  10811  apexp1  10940  ccatsymb  11137  abssubap0  11601  binom  11995  dvds0lem  12312  dvdsnegb  12319  muldvds1  12327  muldvds2  12328  divalgmodcl  12439  gcd2n0cl  12490  lcmdvds  12601  prmdvdsexp  12670  rpexp1i  12676  eqglact  13762  lss0cl  14333  cnpval  14872  cnf2  14879  cnnei  14906  blssec  15112  blpnfctr  15113  mopni2  15157  mopni3  15158  dvply1  15439  uhgrm  15878  upgrm  15900  upgr1or2  15901