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  2881  raltpg  3672  rextpg  3673  disjiun  4025  otexg  4260  opelopabt  4293  tpexg  4476  3optocl  4738  fun2ssres  5298  funssfv  5581  fvun1  5624  foco2  5797  f1elima  5817  eloprabga  6006  caovimo  6114  ot1stg  6207  ot2ndg  6208  ot3rdgg  6209  brtposg  6309  rdgexggg  6432  rdgivallem  6436  nnmass  6542  nndir  6545  nnaword  6566  th3q  6696  ecovass  6700  ecoviass  6701  fpmg  6730  findcard  6946  unfiin  6984  addasspig  7392  mulasspig  7394  mulcanpig  7397  ltapig  7400  ltmpig  7401  addassnqg  7444  ltbtwnnqq  7477  mulnnnq0  7512  addassnq0  7524  genpassl  7586  genpassu  7587  genpassg  7588  aptiprleml  7701  adddir  8012  le2tri3i  8130  addsub12  8234  subdir  8407  reapmul1  8616  recexaplem2  8673  div12ap  8715  divdiv32ap  8741  divdivap1  8744  lble  8968  zaddcllemneg  9359  fnn0ind  9436  xrltso  9865  iccgelb  10001  elicc4  10009  elfz  10083  fzrevral  10174  expnegap0  10621  expgt0  10646  expge0  10649  expge1  10650  mulexpzap  10653  expp1zap  10662  expm1ap  10663  apexp1  10792  abssubap0  11237  binom  11630  dvds0lem  11947  dvdsnegb  11954  muldvds1  11962  muldvds2  11963  divalgmodcl  12072  gcd2n0cl  12109  lcmdvds  12220  prmdvdsexp  12289  rpexp1i  12295  eqglact  13298  lss0cl  13868  cnpval  14377  cnf2  14384  cnnei  14411  blssec  14617  blpnfctr  14618  mopni2  14662  mopni3  14663  dvply1  14943