Theorem 3impa 840

Description: Importation from double to triple conjunction.

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

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787

This theorem is referenced by:  3impdir 893  syl3an9b 903  biimp3a 931  rspec3 1774  rcla43v 1929  mouniss 2947  3optocl 3294  fun2ssres 3610  funssfv 3792  oaword 4241  omord2 4256  omword 4259  omass 4269  oeord 4273  oeword 4275  ecoprass 4381  addasspi 5088  mulasspi 5090  ltapi 5095  ltmpi 5096  genpass 5177  pre-axltadd 5354  pre-axsup 5356  adddir 5384  addsubass 5448  addsub12 5451  subdir 5493  subsub4 5529  leltne 5586  xrleltne 5623  le2tri3i 5654  ltaddsub 5696  leaddsub 5698  recextlem2 5748  divne0b 5790  divassOLD 5803  divdivmul 5853  ltmulgt11 5904  gt0div 5911  ge0div 5912  fldiv2 6369  elfz 6497  fzrevral 6545  seq1cl 6584  absdiflt 6973  absdifle 6974  abssubge0 6985  faclbnd4 7042  faclbnd5 7043  bcval4 7051  fsumspl 7110  clmi2rpi 7178  climsub 7220  caucvglem5 7251  isum1p 7296  expcnv 7323  fsum0diag4 7351  rescncf 7362  absef01tlubi 7478  cos01gt0 7569  infxpabs 7662  basgen2 7728  retopbas 7740  opnneiss 7817  cnf 7847  cnima 7852  cnclima 7856  cnsscnp 7857  cncnp2 7864  metsym 7901  opni3 7951  lpbl 7965  metcnp3 7981  metidcn 7985  metcn4 8056  issubgi 8206  grpsn 8208  ablmul 8215  ghgrpilem4 8220  ghgrpi 8221  nv1 8388  sspnval 8480  lnolin 8499  lnof 8500  nmoge0 8514  nmoub3i 8520  bloln 8528  nmblore 8530  efifolem4 8808  logeftb 8847  explog 8855  hvaddsubass 8993  hvmulcan2 9023  hhssnv 9217  hosval 9599  homval 9601  hodval 9602  hfmval 9605  homco1 9810  homulass 9811  hoadddir 9813  hoaddsubass 9824  hosubsub4 9827  nmopub2tALT 9916  nmfnleub2 9933  adjeq 9942  kbvalval 9961  kbmul 9962  lnopmul 9974  lnopmulsubi 9983  0lnfn 9992  lnopcoi 10011  nmcoplb 10043  nmcfnlb 10072  kbass2 10133  nmopleid 10155  hstoh 10243  mdi 10306  dmdi 10313  dmdi4 10318  mdsl3 10327  cdj3lem2 10446  symggrpi 10491  cayleylem2 10495

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232  df-3an 789

Copyright terms: Public domain