Theorem 3impa 1225

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ex3  1226  3impdir  1335  syl3an9b  1351  biimp3a  1386  stoic3  1480  rspec3  2640  rspc3v  2946  raltpg  3762  rextpg  3763  disjiun  4125  otexg  4372  opelopabt  4406  tpexg  4592  3optocl  4855  fun2ssres  5424  funssfv  5724  fvun1  5772  foco2  5962  f1elima  5982  eloprabga  6178  caovimo  6286  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  brtposg  6530  rdgexggg  6653  rdgivallem  6657  nnmass  6765  nndir  6768  nnaword  6789  th3q  6919  ecovass  6923  ecoviass  6924  fpmg  6960  findcard  7198  unfiin  7239  pr1or2  7546  addasspig  7703  mulasspig  7705  mulcanpig  7708  ltapig  7711  ltmpig  7712  addassnqg  7755  ltbtwnnqq  7788  mulnnnq0  7823  addassnq0  7835  genpassl  7897  genpassu  7898  genpassg  7899  aptiprleml  8012  adddir  8323  le2tri3i  8441  addsub12  8546  subdir  8720  reapmul1  8931  recexaplem2  8988  div12ap  9032  divdiv32ap  9058  divdivap1  9061  lble  9285  zaddcllemneg  9692  fnn0ind  9772  xrltso  10214  iccgelb  10350  elicc4  10358  elfz  10433  fzrevral  10528  expnegap0  11004  expgt0  11029  expge0  11032  expge1  11033  mulexpzap  11036  expp1zap  11045  expm1ap  11046  apexp1  11177  ccatsymb  11391  abssubap0  11878  binom  12275  dvds0lem  12592  dvdsnegb  12599  muldvds1  12607  muldvds2  12608  divalgmodcl  12719  gcd2n0cl  12770  lcmdvds  12881  prmdvdsexp  12951  rpexp1i  12957  eqglact  14086  lss0cl  14814  cnpval  15441  cnf2  15448  cnnei  15475  blssec  15681  blpnfctr  15682  mopni2  15726  mopni3  15727  dvply1  16008  uhgrm  16541  upgrm  16563  upgr1or2  16564