HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 3adant3 797
Description: Deduction adding a conjunct to antecedent.
Hypothesis
Ref Expression
3adant.1 |- ((ph /\ ps) -> ch)
Assertion
Ref Expression
3adant3 |- ((ph /\ ps /\ th) -> ch)
Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 783 . 2 |- ((ph /\ ps /\ th) -> (ph /\ ps))
2 3adant.1 . 2 |- ((ph /\ ps) -> ch)
31, 2syl 10 1 |- ((ph /\ ps /\ th) -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773
This theorem is referenced by:  3adantl3 803  wereu 2935  ordunel 3074  funopg 3533  fnco 3581  f1ocnvfvb 3866  f1ofveu 3867  oprabvalig 4009  oprabval6g 4017  curry1val 4084  oaword 4167  omord2 4182  omcan 4184  omword 4185  omwordi 4186  oneo 4196  oeord 4199  oecan 4200  oeword 4201  oewordi 4202  ecopoprtrn 4295  eceqopreq 4297  abfii2 4536  zfregs 4619  ltsopi 4988  ltsopq 5047  genpass 5084  ltsopr 5108  ltsosr 5175  ltasr 5181  ltsor 5233  add12t 5308  addcan2t 5325  addsubt 5356  npncant 5372  nppcant 5373  subcant 5384  mul12t 5390  subdit 5399  nnncan1t 5439  ppncant 5453  axlttrn 5476  axltadd 5477  ltso 5484  lelttrt 5496  xrltso 5527  xrlelttrt 5535  xrre2t 5543  ltaddsub2t 5606  leaddsub2t 5608  lesub2t 5634  ltsub2t 5636  recextlem2 5656  div23t 5705  divcan4t 5719  divsubdirt 5731  divcan5t 5737  letrp1t 5772  lemul1t 5788  lemul1it 5793  lemul1itOLD 5794  ltmulgt12t 5803  lediv1t 5806  ltmuldiv2t 5818  lt2mul2divt 5822  lemuldivt 5824  lemuldiv2t 5825  ltdiv2t 5835  lediv2t 5839  xrmaxltt 5861  maxlet 5866  maxltt 5870  nndivtrt 5907  lbinfmle 5997  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  supxrun 6032  qsqueeze 6218  seq1rn2 6258  shftval2t 6284  shftf 6288  iooss2 6311  iccsupr 6331  lbicc2t 6337  ubicc2t 6338  ioonegt 6339  iccnegt 6340  icoshft 6341  infmssuzle 6397  fzrevral2t 6452  fzshftralt 6454  seqzp1 6480  seqzval2t 6485  expsubt 6529  expordit 6531  expwordit 6534  expword2it 6536  exple1t 6538  expubndt 6539  bernneq2 6584  abssubne0t 6820  abssubge0t 6833  abssuble0t 6834  caure 6864  cauim 6865  ser1absdif 6867  bcval2t 6897  bccmplt 6900  fsum1ps 6956  fsum0split 6959  fsumshft 6969  fsumshftm 6970  serz1p 6990  serzsplit 6994  climmullem3 7058  climmullem4 7059  climmullem5 7060  iserzgt0 7146  expcnv 7168  geoisum1c 7180  cvgratlem5 7189  rescncf 7207  cncffvrn 7208  mulc1cncf 7214  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  sin01gt0 7418  cos01gt0 7419  sin02gt0 7420  tgss2t 7579  clsss 7629  clsss2 7645  elcls 7646  ntrcls0 7649  neiint 7660  neiss 7664  neips 7668  opnssneib 7670  innei 7677  islp2 7688  cnpval 7699  iscnp 7700  cncnp 7717  cncnp2 7718  metsym 7755  metxplem3 7768  metxplem4 7773  blin 7792  ssbl 7795  methausi 7820  metcnpf 7822  metcnf 7823  metcnp 7826  metcnss 7837  metdnsconst 7840  cnmet 7843  bl2ioo 7850  ioo2bl 7851  blssioo 7852  tgioolem 7853  dscmet 7856  lmbrf 7868  lmuni 7886  iscms2lem3 7925  iscms2lem4 7926  grpinvid1 8006  grpinvid2 8007  grpasscan1OLD 8008  grpasscan1 8012  grpinvop 8015  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  grplactval 8033  ablnncan 8049  issubgi 8059  ablmul 8068  ghgrpilem4 8073  ringsn 8100  vcsubdir 8112  vcnegsubdi2 8131  vcoprnelem 8135  isvc 8138  isnv 8170  nvscom 8190  nvmul0or 8212  nvpncan2 8216  nvaddsub4 8221  nvnncan 8223  nvdif 8232  nvpi 8233  nvabs 8240  nv1 8243  imsmetlem 8261  nvelbl 8263  nvcnf 8265  va1cnlem 8279  nmoval 8358  0oval 8380  blometi 8394  ipasslem5 8425  hlipgt0 8546  ssphl 8549  pslem 8573  psasym 8576  spwval3 8578  spwnex3 8579  pilem1 8590  sinq12gt0t 8625  sincosq1eq 8626  efifolem5 8641  efif1lem1 8645  efif1lem2 8646  circgrpOLD 8658  explogt 8694  grothinf 8720  hvadd12t 8825  hvmulcomt 8833  hvsubdistr1t 8837  hvsubdistr2t 8838  hvaddcan2t 8859  hvmulcant 8860  hvmulcan2t 8861  hvsubcant 8862  hvsubcan2t 8863  his7t 8877  his2subt 8879  his2sub2t 8880  bcs2t 8970  bcs3t 8971  hcau2 8976  hhssnv 9054  projlem26 9127  chj12t 9372  spansncol 9407  pjspansnt 9417  cm2jt 9480  homul12t 9648  hoaddsubt 9659  unopf1ot 9756  adj2t 9774  braaddt 9785  eigvalclt 9801  lnopmulsub 9816  hmopcot 9863  nmcopexlem5 9870  nmcfnexlem5 9899  cnlnadjlem2 9916  adjlnopt 9934  kbass2t 9962  leopmult 9979  hstoht 10069  strlem3a 10089  hstrlem3a 10097  cvntrt 10129  dmdsl3t 10150  atexcht 10216  atcvatlem 10220  mdsymlem5 10242  cdj3lem2 10267  cdj3lem3 10270  lediv2itALT 10276  ghomgsg 10300  ghomf1olem 10301  symggrpiOLD 10311  symggrpi 10313  elo 10345  infi1 10347  cnrscoa 10397  ishomeo 10404  cmphmp 10408  cnvhmpha 10412  cnvhmphb 10413  hmphtr 10418  hmeogrp 10425  homcard 10426  neifil 10442  filintf 10443  cnfilca 10451  dmse1 10467  mslb1 10473  msra3 10475  eqidob 10567  cmphmib 10571  cmpassoh 10573  cmpmon 10585  isfunb 10593
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