Theorem 3impa 1184

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

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

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

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

This theorem is referenced by:  ex3  1185  3impdir  1284  syl3an9b  1300  biimp3a  1335  stoic3  1419  rspec3  2556  rspc3v  2846  raltpg  3629  rextpg  3630  disjiun  3977  otexg  4208  opelopabt  4240  tpexg  4422  3optocl  4682  fun2ssres  5231  funssfv  5512  fvun1  5552  foco2  5722  f1elima  5741  eloprabga  5929  caovimo  6035  ot1stg  6120  ot2ndg  6121  ot3rdgg  6122  brtposg  6222  rdgexggg  6345  rdgivallem  6349  nnmass  6455  nndir  6458  nnaword  6479  th3q  6606  ecovass  6610  ecoviass  6611  fpmg  6640  findcard  6854  unfiin  6891  addasspig  7271  mulasspig  7273  mulcanpig  7276  ltapig  7279  ltmpig  7280  addassnqg  7323  ltbtwnnqq  7356  mulnnnq0  7391  addassnq0  7403  genpassl  7465  genpassu  7466  genpassg  7467  aptiprleml  7580  adddir  7890  le2tri3i  8007  addsub12  8111  subdir  8284  reapmul1  8493  recexaplem2  8549  div12ap  8590  divdiv32ap  8616  divdivap1  8619  lble  8842  zaddcllemneg  9230  fnn0ind  9307  xrltso  9732  iccgelb  9868  elicc4  9876  elfz  9950  fzrevral  10040  expnegap0  10463  expgt0  10488  expge0  10491  expge1  10492  mulexpzap  10495  expp1zap  10504  expm1ap  10505  apexp1  10631  abssubap0  11032  binom  11425  dvds0lem  11741  dvdsnegb  11748  muldvds1  11756  muldvds2  11757  divalgmodcl  11865  gcd2n0cl  11902  lcmdvds  12011  prmdvdsexp  12080  rpexp1i  12086  cnpval  12838  cnf2  12845  cnnei  12872  blssec  13078  blpnfctr  13079  mopni2  13123  mopni3  13124