Theorem 3impa 1139

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 357	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1138	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 925

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 927

This theorem is referenced by:  3impdir  1231  syl3an9b  1247  biimp3a  1282  stoic3  1366  rspec3  2464  rspc3v  2738  raltpg  3499  rextpg  3500  disjiun  3846  otexg  4066  opelopabt  4098  tpexg  4279  3optocl  4529  fun2ssres  5070  funssfv  5343  fvun1  5383  foco2  5547  f1elima  5566  eloprabga  5749  caovimo  5852  ot1stg  5937  ot2ndg  5938  ot3rdgg  5939  brtposg  6033  rdgexggg  6156  rdgivallem  6160  nnmass  6262  nndir  6265  nnaword  6284  th3q  6411  ecovass  6415  ecoviass  6416  fpmg  6445  findcard  6658  unfiin  6690  addasspig  6950  mulasspig  6952  mulcanpig  6955  ltapig  6958  ltmpig  6959  addassnqg  7002  ltbtwnnqq  7035  mulnnnq0  7070  addassnq0  7082  genpassl  7144  genpassu  7145  genpassg  7146  aptiprleml  7259  adddir  7540  le2tri3i  7654  addsub12  7756  subdir  7925  reapmul1  8133  recexaplem2  8182  div12ap  8222  divdiv32ap  8248  divdivap1  8251  lble  8469  zaddcllemneg  8850  fnn0ind  8923  xrltso  9327  iccgelb  9411  elicc4  9419  elfz  9491  fzrevral  9580  expnegap0  10024  expgt0  10049  expge0  10052  expge1  10053  mulexpzap  10056  expp1zap  10065  expm1ap  10066  abssubap0  10584  binom  10939  dvds0lem  11145  dvdsnegb  11152  muldvds1  11160  muldvds2  11161  divalgmodcl  11267  gcd2n0cl  11300  lcmdvds  11400  prmdvdsexp  11466  rpexp1i  11472