Theorem 3impa 1177

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

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

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 965

This theorem is referenced by:  3impdir  1276  syl3an9b  1292  biimp3a  1327  stoic3  1411  rspec3  2547  rspc3v  2832  raltpg  3612  rextpg  3613  disjiun  3960  otexg  4190  opelopabt  4222  tpexg  4404  3optocl  4664  fun2ssres  5213  funssfv  5494  fvun1  5534  foco2  5704  f1elima  5723  eloprabga  5908  caovimo  6014  ot1stg  6100  ot2ndg  6101  ot3rdgg  6102  brtposg  6201  rdgexggg  6324  rdgivallem  6328  nnmass  6434  nndir  6437  nnaword  6458  th3q  6585  ecovass  6589  ecoviass  6590  fpmg  6619  findcard  6833  unfiin  6870  addasspig  7250  mulasspig  7252  mulcanpig  7255  ltapig  7258  ltmpig  7259  addassnqg  7302  ltbtwnnqq  7335  mulnnnq0  7370  addassnq0  7382  genpassl  7444  genpassu  7445  genpassg  7446  aptiprleml  7559  adddir  7869  le2tri3i  7985  addsub12  8088  subdir  8261  reapmul1  8470  recexaplem2  8526  div12ap  8567  divdiv32ap  8593  divdivap1  8596  lble  8818  zaddcllemneg  9206  fnn0ind  9280  xrltso  9703  iccgelb  9836  elicc4  9844  elfz  9918  fzrevral  10007  expnegap0  10427  expgt0  10452  expge0  10455  expge1  10456  mulexpzap  10459  expp1zap  10468  expm1ap  10469  apexp1  10592  abssubap0  10990  binom  11381  dvds0lem  11697  dvdsnegb  11704  muldvds1  11712  muldvds2  11713  divalgmodcl  11819  gcd2n0cl  11853  lcmdvds  11956  prmdvdsexp  12023  rpexp1i  12029  cnpval  12609  cnf2  12616  cnnei  12643  blssec  12849  blpnfctr  12850  mopni2  12894  mopni3  12895