Theorem 3impa 1189

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

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

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 975

This theorem is referenced by:  ex3  1190  3impdir  1289  syl3an9b  1305  biimp3a  1340  stoic3  1424  rspec3  2560  rspc3v  2850  raltpg  3636  rextpg  3637  disjiun  3984  otexg  4215  opelopabt  4247  tpexg  4429  3optocl  4689  fun2ssres  5241  funssfv  5522  fvun1  5562  foco2  5733  f1elima  5752  eloprabga  5940  caovimo  6046  ot1stg  6131  ot2ndg  6132  ot3rdgg  6133  brtposg  6233  rdgexggg  6356  rdgivallem  6360  nnmass  6466  nndir  6469  nnaword  6490  th3q  6618  ecovass  6622  ecoviass  6623  fpmg  6652  findcard  6866  unfiin  6903  addasspig  7292  mulasspig  7294  mulcanpig  7297  ltapig  7300  ltmpig  7301  addassnqg  7344  ltbtwnnqq  7377  mulnnnq0  7412  addassnq0  7424  genpassl  7486  genpassu  7487  genpassg  7488  aptiprleml  7601  adddir  7911  le2tri3i  8028  addsub12  8132  subdir  8305  reapmul1  8514  recexaplem2  8570  div12ap  8611  divdiv32ap  8637  divdivap1  8640  lble  8863  zaddcllemneg  9251  fnn0ind  9328  xrltso  9753  iccgelb  9889  elicc4  9897  elfz  9971  fzrevral  10061  expnegap0  10484  expgt0  10509  expge0  10512  expge1  10513  mulexpzap  10516  expp1zap  10525  expm1ap  10526  apexp1  10652  abssubap0  11054  binom  11447  dvds0lem  11763  dvdsnegb  11770  muldvds1  11778  muldvds2  11779  divalgmodcl  11887  gcd2n0cl  11924  lcmdvds  12033  prmdvdsexp  12102  rpexp1i  12108  cnpval  12992  cnf2  12999  cnnei  13026  blssec  13232  blpnfctr  13233  mopni2  13277  mopni3  13278