Theorem 3adant3 801

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
3adant.1	⊢ ((φ ⋀ ψ) → χ)

Assertion

Ref	Expression
3adant3	⊢ ((φ ⋀ ψ ⋀ θ) → χ)

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 787	. 2 ⊢ ((φ ⋀ ψ ⋀ θ) → (φ ⋀ ψ))
2		3adant.1	. 2 ⊢ ((φ ⋀ ψ) → χ)
3	1, 2	syl 10	1 ⊢ ((φ ⋀ ψ ⋀ θ) → χ)

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 777

This theorem is referenced by:  3adantl3 807  wereu 2951  ordunel 3090  funopg 3553  fnco 3601  f1ocnvfvb 3887  f1ofveu 3888  oprabvalig 4030  oprabval6g 4038  curry1val 4106  oaword 4189  omord2 4204  omcan 4206  omword 4207  omwordi 4208  oneo 4218  oeord 4221  oecan 4222  oeword 4223  oewordi 4224  ecopoprtrn 4317  eceqopreq 4319  zfregs 4657  ltsopi 5028  ltsopq 5087  genpass 5124  ltsopr 5148  ltsosr 5215  ltasr 5221  ltsor 5273  add12t 5348  addcan2t 5365  addsubt 5396  npncant 5412  nppcant 5413  subcant 5424  mul12t 5430  subdit 5439  nnncan1t 5479  ppncant 5493  axlttrn 5516  axltadd 5517  ltso 5524  lelttrt 5535  xrltso 5566  xrlelttrt 5574  xrre2t 5582  ltaddsub2t 5644  leaddsub2t 5646  lesub2t 5673  ltsub2t 5675  recextlem2 5695  div23t 5749  divcan4t 5764  divsubdirt 5776  divsubdirtOLD 5777  divcan5t 5783  letrp1t 5818  lemul1t 5834  lemul1it 5839  lemul1itOLD 5840  ltmulgt12t 5849  lediv1t 5853  lediv1tOLD 5854  ltmuldiv2tOLD 5868  lt2mul2divt 5874  lemuldivtOLD 5877  lemuldiv2tOLD 5879  ltdiv2t 5889  lediv2t 5893  xrmaxltt 5915  maxlet 5920  maxltt 5924  nndivtrt 5962  lbinfmle 6052  infmrcl 6071  xrsupsslem 6078  xrinfmsslem 6079  supxrre 6085  supxrun 6087  qsqueeze 6281  seq1rn2 6322  shftval2t 6348  shftf 6352  iooss2 6375  elioo5t 6385  iccsupr 6399  lbicc2t 6405  ubicc2t 6406  iccnegt 6408  icoshft 6409  ioojoint 6417  infmssuzle 6466  fzrevral2t 6521  fzshftralt 6523  seqzp1 6549  seqzval2t 6554  expsubt 6599  expordit 6601  expwordit 6604  expword2it 6606  exple1t 6608  expubndt 6609  bernneq2 6654  abssubne0t 6882  abssubge0t 6895  abssuble0t 6896  caure 6927  cauim 6928  ser1absdif 6930  bcval2t 6959  bccmplt 6962  fsum1ps 7018  fsum0split 7021  fsumshft 7031  fsumshftm 7032  serz1p 7052  serzsplit 7056  climmullem3 7122  climmullem4 7123  climmullem5 7124  iserzgt0 7211  expcnv 7233  geoisum1c 7245  cvgratlem5 7254  rescncf 7272  cncffvrn 7273  mulc1cncf 7279  ivthlem6 7286  ivthlem7 7287  sin01gt0 7477  cos01gt0 7478  sin02gt0 7479  tgss2t 7636  clsss 7684  clsss2 7700  elcls 7701  ntrcls0 7704  neiint 7716  neiss 7720  neips 7724  opnssneib 7726  innei 7733  islp2 7744  cnpval 7756  iscnp 7757  cncnp 7775  cncnp2 7776  metsym 7813  metxplem3 7825  metxplem4 7830  blin 7849  ssbl 7852  methausi 7878  metcnpf 7880  metcnf 7881  metcnp 7884  metcnss 7895  metdnsconst 7898  cnmet 7901  bl2ioo 7908  ioo2bl 7909  blssioo 7910  tgioolem 7911  dscmet 7915  lmbrf 7927  lmuni 7948  iscms2lem3 7988  iscms2lem4 7989  grpinvid1 8068  grpinvid2 8069  grpasscan1 8073  grpinvop 8076  grppncan 8086  grpnpcan 8087  grppnpcan2 8088  grplactval 8093  ablnncan 8108  issubgi 8118  ablmul 8127  ghgrpilem4 8132  ringsn 8159  vcsubdir 8171  vcnegsubdi2 8190  vcoprnelem 8193  isvc 8196  isnv 8227  nvscom 8246  nvmul0or 8268  nvpncan2 8272  nvaddsub4 8277  nvnncan 8279  nvdif 8289  nvpi 8290  nvabs 8297  nv1 8300  imsmetlem 8319  nvelbl 8321  nvcnf 8323  nvcnpf 8324  va1cnlem 8341  nmoval 8422  0oval 8444  lnon0 8454  blometi 8459  ipasslem5 8490  hlipgt0 8612  ssphl 8615  pslem 8643  psasym 8647  pstr 8648  spwval3 8650  spwnex3 8651  spwpr4OLD 8658  spwpr4aOLD 8659  pilem1 8666  sinq12gt0t 8703  sincosq1eq 8704  efifolem5 8721  efif1lem1 8725  efif1lem2 8726  explogt 8767  grothinf 8776  hvadd12t 8899  hvmulcomt 8907  hvsubdistr1t 8911  hvsubdistr2t 8912  hvaddcan2t 8933  hvmulcant 8934  hvmulcan2t 8935  hvsubcant 8936  hvsubcan2t 8937  his7t 8951  his2subt 8953  his2sub2t 8954  bcs2t 9044  bcs3t 9045  hcau2 9050  hhssnv 9129  projlem26 9206  chj12t 9452  spansncol 9486  pjspansnt 9495  cm2jt 9558  homul12t 9726  hoaddsubt 9737  unopf1ot 9835  adj2t 9853  braaddt 9864  eigvalclt 9880  lnopmulsub 9895  hmopcot 9943  nmcopexlem5 9950  nmcfnexlem5 9979  cnlnadjlem2 9996  adjlnopt 10014  kbass2t 10045  leopmult 10062  leoptrt 10065  hstoht 10154  strlem3a 10174  hstrlem3a 10182  cvntrt 10214  dmdsl3t 10237  atexcht 10303  atcvatlem 10307  mdsymlem5 10329  cdj3lem2 10357  cdj3lem3 10360  lediv2itALT 10366  ghomgsg 10390  ghomf1olem 10391  symggrpi 10401  elo 10439  infi1 10441  cnrscoa 10496  ishomeo 10503  cmphmp 10507  cnvhmpha 10511  cnvhmphb 10512  hmphtr 10517  hmeogrp 10524  homcard 10525  hmeobc 10528  neifil 10553  filintf 10554  cnfilca 10562  sfvlim 10576  plimfilOLD 10580  dmse1 10594  mslb1 10600  msra3 10602  eqidob 10694  cmphmib 10698  cmpassoh 10700  cmpmon 10714  isfunb 10726

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 779

Copyright terms: Public domain