Theorem 3impa 828

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

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

This theorem is referenced by:  3impdir 881  syl3an9b 891  biimp3a 919  rspec3 1727  rcla43v 1882  mouniss 2890  3optocl 3237  fun2ssres 3553  funssfv 3735  oaword 4183  omord2 4198  omword 4201  omass 4211  oeord 4215  oeword 4217  ecoprass 4320  addasspi 5023  mulasspi 5025  ltapi 5030  ltmpi 5031  genpass 5112  pre-axltadd 5289  pre-axsup 5291  adddirt 5319  addsubasst 5383  addsub12t 5386  subdirt 5428  subsub4t 5464  leltnet 5521  xrleltnet 5558  le2tri3 5589  ltaddsubt 5631  leaddsubt 5633  recextlem2 5683  divne0bt 5728  divasst 5741  divdivmult 5795  ltmulgt11t 5846  gt0divt 5853  ge0divt 5854  seq1cl 6325  elfzt 6471  fzrevralt 6519  absdifltt 6883  absdiflet 6884  abssubge0t 6895  faclbnd4 6952  faclbnd5 6953  bcval4t 6961  fsumsplit 7020  clmi2rp 7088  climsub 7130  caucvglem5 7161  isum1p 7206  expcnv 7233  fsum0diag4 7261  rescncf 7272  absef01tlub 7388  cos01gt0 7477  infxpabs 7570  basgen2t 7639  retopbas 7655  opnneiss 7732  cnf 7762  cnima 7767  cnclima 7771  cnsscnp 7772  cncnp2 7779  metsym 7816  opni3 7866  lpbl 7880  metcnp3 7896  metidcn 7900  metcn4 7971  issubgi 8122  grpsn 8124  ablmul 8131  ghgrpilem4 8136  ghgrpi 8137  nv1 8304  sspnval 8396  lnolin 8415  lnof 8416  nmoge0 8430  nmoub3i 8436  bloln 8444  nmblore 8446  efifolem4 8725  logeftb 8764  explogt 8772  hvaddsubasst 8910  hvmulcan2t 8940  hhssnv 9134  hosvalt 9516  homvalt 9518  hodvalt 9519  hfmvalt 9522  homco1t 9727  homulasst 9728  hoadddirt 9730  hoaddsubasst 9741  hosubsub4t 9744  nmopub2tALT 9833  nmfnleub2t 9850  adjeqt 9859  kbvalvalt 9878  kbmult 9879  lnopmult 9891  lnopmulsub 9900  0lnfn 9909  lnopco 9928  nmcoplbt 9960  nmcfnlbt 9989  kbass2t 10050  nmopleidt 10072  hstoht 10159  mdit 10222  dmdit 10229  dmdi4 10234  mdsl3t 10243  cdj3lem2 10362  symggrpi 10406  cayleylem2 10410

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 777

Copyright terms: Public domain