Theorem 3impa 827

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

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774

This theorem is referenced by:  3impdir 879  syl3an9b 889  biimp3a 917  rspec3 1724  rcla43v 1878  mouniss 2885  3optocl 3232  fun2ssres 3545  funssfv 3726  oaword 4173  omord2 4188  omword 4191  omass 4201  oeord 4205  oeword 4207  ecoprass 4310  addasspi 5003  mulasspi 5005  ltapi 5010  ltmpi 5011  genpass 5092  pre-axltadd 5269  pre-axsup 5271  adddirt 5299  addsubasst 5363  addsub12t 5366  subdirt 5408  subsub4t 5444  leltnet 5502  xrleltnet 5539  le2tri3 5571  ltaddsubt 5613  leaddsubt 5615  recextlem2 5664  divne0bt 5699  divasst 5712  divdivmult 5759  ltmulgt11t 5810  gt0divt 5815  ge0divt 5816  seq1cl 6270  elfzt 6411  fzrevralt 6459  absdifltt 6829  absdiflet 6830  abssubge0t 6841  faclbnd4 6897  faclbnd5 6898  bcval4t 6907  fsumsplit 6966  clmi2rp 7034  climsub 7074  caucvglem5 7105  isum1p 7149  expcnv 7176  fsum0diag4 7204  rescncf 7215  absef01tlub 7337  cos01gt0 7427  infxpabs 7521  basgen2t 7589  retopbas 7605  opnneiss 7682  cnf 7712  cnima 7717  cnclima 7721  cnsscnp 7722  cncnp2 7729  metsym 7766  opni3 7818  lpbl 7832  metcnp3 7848  metidcn 7852  metcn4 7921  resgrprnOLD 8046  issubgi 8074  grpsn 8076  ablmul 8083  ghgrpilem4 8088  ghgrpi 8089  nv1 8256  sspnval 8343  lnolin 8362  lnof 8363  nmoge0 8375  nmoub3i 8381  bloln 8389  nmblore 8391  efifolem4 8659  circgrpOLD 8677  logeftb 8703  explogt 8711  hvaddsubasst 8849  hvmulcan2t 8879  hhssnv 9073  hosvalt 9456  homvalt 9458  hodvalt 9459  hfmvalt 9462  homco1t 9667  homulasst 9668  hoadddirt 9670  hoaddsubasst 9681  hosubsub4t 9684  nmopub2tALT 9773  nmfnleub2t 9789  adjeqt 9798  kbvalvalt 9817  kbmult 9818  lnopmult 9830  lnopmulsub 9839  0lnfn 9848  lnopco 9866  nmcoplbt 9898  nmcfnlbt 9927  kbass2t 9988  nmopleidt 10010  hstoht 10097  mdit 10160  dmdit 10167  dmdi4 10172  mdsl3t 10180  cdj3lem2 10296  symggrpi 10340  cayleylem2 10344

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 147  df-an 225  df-3an 776

Copyright terms: Public domain