Theorem 3impa 1196

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

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

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 982

This theorem is referenced by:  ex3  1197  3impdir  1305  syl3an9b  1321  biimp3a  1356  stoic3  1442  rspec3  2584  rspc3v  2880  raltpg  3671  rextpg  3672  disjiun  4024  otexg  4259  opelopabt  4292  tpexg  4475  3optocl  4737  fun2ssres  5297  funssfv  5580  fvun1  5623  foco2  5796  f1elima  5816  eloprabga  6005  caovimo  6112  ot1stg  6205  ot2ndg  6206  ot3rdgg  6207  brtposg  6307  rdgexggg  6430  rdgivallem  6434  nnmass  6540  nndir  6543  nnaword  6564  th3q  6694  ecovass  6698  ecoviass  6699  fpmg  6728  findcard  6944  unfiin  6982  addasspig  7390  mulasspig  7392  mulcanpig  7395  ltapig  7398  ltmpig  7399  addassnqg  7442  ltbtwnnqq  7475  mulnnnq0  7510  addassnq0  7522  genpassl  7584  genpassu  7585  genpassg  7586  aptiprleml  7699  adddir  8010  le2tri3i  8128  addsub12  8232  subdir  8405  reapmul1  8614  recexaplem2  8671  div12ap  8713  divdiv32ap  8739  divdivap1  8742  lble  8966  zaddcllemneg  9356  fnn0ind  9433  xrltso  9862  iccgelb  9998  elicc4  10006  elfz  10080  fzrevral  10171  expnegap0  10618  expgt0  10643  expge0  10646  expge1  10647  mulexpzap  10650  expp1zap  10659  expm1ap  10660  apexp1  10789  abssubap0  11234  binom  11627  dvds0lem  11944  dvdsnegb  11951  muldvds1  11959  muldvds2  11960  divalgmodcl  12069  gcd2n0cl  12106  lcmdvds  12217  prmdvdsexp  12286  rpexp1i  12292  eqglact  13295  lss0cl  13865  cnpval  14366  cnf2  14373  cnnei  14400  blssec  14606  blpnfctr  14607  mopni2  14651  mopni3  14652