Theorem 3impa 1194

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

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

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 980

This theorem is referenced by:  ex3  1195  3impdir  1294  syl3an9b  1310  biimp3a  1345  stoic3  1431  rspec3  2567  rspc3v  2858  raltpg  3646  rextpg  3647  disjiun  3999  otexg  4231  opelopabt  4263  tpexg  4445  3optocl  4705  fun2ssres  5260  funssfv  5542  fvun1  5583  foco2  5755  f1elima  5774  eloprabga  5962  caovimo  6068  ot1stg  6153  ot2ndg  6154  ot3rdgg  6155  brtposg  6255  rdgexggg  6378  rdgivallem  6382  nnmass  6488  nndir  6491  nnaword  6512  th3q  6640  ecovass  6644  ecoviass  6645  fpmg  6674  findcard  6888  unfiin  6925  addasspig  7329  mulasspig  7331  mulcanpig  7334  ltapig  7337  ltmpig  7338  addassnqg  7381  ltbtwnnqq  7414  mulnnnq0  7449  addassnq0  7461  genpassl  7523  genpassu  7524  genpassg  7525  aptiprleml  7638  adddir  7948  le2tri3i  8066  addsub12  8170  subdir  8343  reapmul1  8552  recexaplem2  8609  div12ap  8651  divdiv32ap  8677  divdivap1  8680  lble  8904  zaddcllemneg  9292  fnn0ind  9369  xrltso  9796  iccgelb  9932  elicc4  9940  elfz  10014  fzrevral  10105  expnegap0  10528  expgt0  10553  expge0  10556  expge1  10557  mulexpzap  10560  expp1zap  10569  expm1ap  10570  apexp1  10698  abssubap0  11099  binom  11492  dvds0lem  11808  dvdsnegb  11815  muldvds1  11823  muldvds2  11824  divalgmodcl  11933  gcd2n0cl  11970  lcmdvds  12079  prmdvdsexp  12148  rpexp1i  12154  eqglact  13084  cnpval  13701  cnf2  13708  cnnei  13735  blssec  13941  blpnfctr  13942  mopni2  13986  mopni3  13987