Theorem 3impa 1099

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 346	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1098	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3impdir  1191  syl3an9b  1205  biimp3a  1235  stoic3  1320  rspec3  2409  rspc3v  2665  raltpg  3423  rextpg  3424  otexg  3967  opelopabt  3999  tpexg  4179  3optocl  4418  fun2ssres  4943  funssfv  5199  fvun1  5239  foco2  5318  f1elima  5412  eloprabga  5591  caovimo  5694  ot1stg  5779  ot2ndg  5780  ot3rdgg  5781  brtposg  5869  rdgexggg  5964  rdgivallem  5968  frecsuclem1  5987  nnmass  6066  nndir  6069  nnaword  6084  th3q  6211  ecovass  6215  ecoviass  6216  findcard  6345  addasspig  6428  mulasspig  6430  mulcanpig  6433  ltapig  6436  ltmpig  6437  addassnqg  6480  ltbtwnnqq  6513  mulnnnq0  6548  addassnq0  6560  genpassl  6622  genpassu  6623  genpassg  6624  aptiprleml  6737  adddir  7018  le2tri3i  7126  addsub12  7224  subdir  7383  reapmul1  7586  recexaplem2  7633  div12ap  7673  divdiv32ap  7696  divdivap1  7699  zaddcllemneg  8284  fnn0ind  8354  xrltso  8717  iccgelb  8801  elicc4  8809  elfz  8880  fzrevral  8967  expivallem  9256  expnegap0  9263  expgt0  9288  expge0  9291  expge1  9292  mulexpzap  9295  expp1zap  9303  expm1ap  9304  abssubap0  9686