Theorem 3impa 826

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

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

This theorem is referenced by:  3impdir 878  syl3an9b 888  biimp3a 916  rspec3 1719  rcla43v 1873  mouniss 2880  3optocl 3227  fun2ssres 3539  funssfv 3720  oaword 4167  omord2 4182  omword 4185  omass 4195  oeord 4199  oeword 4201  ecoprass 4304  addasspi 4995  mulasspi 4997  ltapi 5002  ltmpi 5003  genpass 5084  pre-axltadd 5261  pre-axsup 5263  adddirt 5291  addsubasst 5355  addsub12t 5358  subdirt 5400  subsub4t 5436  leltnet 5494  xrleltnet 5531  le2tri3 5563  ltaddsubt 5605  leaddsubt 5607  recextlem2 5656  divne0bt 5691  divasst 5704  divdivmult 5751  ltmulgt11t 5802  gt0divt 5807  ge0divt 5808  seq1cl 6262  elfzt 6403  fzrevralt 6451  absdifltt 6821  absdiflet 6822  abssubge0t 6833  faclbnd4 6889  faclbnd5 6890  bcval4t 6899  fsumsplit 6958  clmi2rp 7026  climsub 7066  caucvglem5 7097  isum1p 7141  expcnv 7168  fsum0diag4 7196  rescncf 7207  absef01tlub 7329  cos01gt0 7419  infxpabs 7513  basgen2t 7581  retopbas 7597  opnneiss 7673  cnf 7701  cnima 7706  cnclima 7710  cnsscnp 7711  cncnp2 7718  metsym 7755  opni3 7806  lpbl 7819  metcnp3 7835  metidcn 7839  metcn4 7905  resgrprnOLD 8031  issubgi 8059  grpsn 8061  ablmul 8068  ghgrpilem4 8073  ghgrpi 8074  nv1 8243  sspnval 8330  lnolin 8349  lnof 8350  nmoge0 8362  nmoub3i 8368  bloln 8376  nmblore 8378  efifolem4 8640  circgrpOLD 8658  logeftb 8686  explogt 8694  hvaddsubasst 8831  hvmulcan2t 8861  hhssnv 9054  hosvalt 9433  homvalt 9435  hodvalt 9436  hfmvalt 9439  homco1t 9644  homulasst 9645  hoadddirt 9647  hoaddsubasst 9658  hosubsub4t 9661  nmopub2tALT 9750  nmfnleub2t 9766  adjeqt 9775  kbvalvalt 9794  kbmult 9795  lnopmult 9807  lnopmulsub 9816  0lnfn 9825  lnopco 9843  nmcoplbt 9875  nmcfnlbt 9904  kbass2t 9962  nmopleidt 9983  hstoht 10069  mdit 10132  dmdit 10139  dmdi4 10143  mdsl3t 10151  cdj3lem2 10267  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317

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 775

Copyright terms: Public domain