ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3adant3 GIF version

Theorem 3adant3 986
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
3adant3 ((𝜑𝜓𝜃) → 𝜒)

Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 963 . 2 ((𝜑𝜓𝜃) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  stoic4a  1393  stoic4b  1394  vtoclgft  2710  eqeu  2827  tpssi  3656  issod  4211  sotricim  4215  soinxp  4579  funopg  5127  fnco  5201  resasplitss  5272  resdif  5357  fnimapr  5449  ftpg  5572  fsnunfv  5589  fvpr1g  5594  fvpr2g  5595  f1ocnvfvb  5649  f1oiso2  5696  moriotass  5726  f1ofveu  5730  acexmid  5741  ovig  5860  ov6g  5876  ovg  5877  ot1stg  6018  ot2ndg  6019  poxp  6097  brtposg  6119  smores3  6158  smoiso  6167  rdgivallem  6246  frecsuclem  6271  nnaord  6373  nnaword  6375  nnawordex  6392  ecopovtrn  6494  ecopovtrng  6497  xpdom3m  6696  mapxpen  6710  sbthlemi4  6816  djuenun  7036  ltsopi  7096  addcanpig  7110  distrnqg  7163  ltsonq  7174  ltanqg  7176  ltmnqg  7177  nnanq0  7234  distrnq0  7235  distnq0r  7239  prarloclem  7277  genpassl  7300  genpassu  7301  distrlem1prl  7358  distrlem1pru  7359  distrlem5prl  7362  distrlem5pru  7363  1idprl  7366  1idpru  7367  ltpopr  7371  ltsopr  7372  ltexprlemm  7376  ltexprlemfl  7385  ltexprlemfu  7387  addcanprlemu  7391  recexprlem1ssl  7409  recexprlem1ssu  7410  aptipr  7417  lttrsr  7538  ltsosr  7540  ltasrg  7546  recexgt0sr  7549  mulextsr1  7557  axmulass  7649  ltxrlt  7798  axltwlin  7800  axlttrn  7801  axltadd  7802  letr  7815  mul12  7859  add12  7888  subadd  7933  addsub  7941  npncan  7951  nppcan  7952  nnpcan  7953  nppcan3  7954  pnpcan  7969  pnncan  7971  ppncan  7972  subdi  8115  ltaddsub2  8167  leaddsub2  8169  ltaddsublt  8300  apreap  8316  lemul1  8322  reapmul1lem  8323  reapadd1  8325  reapcotr  8327  receuap  8397  divassap  8417  div23ap  8418  divmulassap  8422  divmulasscomap  8423  divcanap4  8426  divsubdirap  8435  divcanap5  8441  divdiv32ap  8447  divdivap2  8451  div2subap  8563  letrp1  8570  ltmulgt12  8587  lediv1  8591  ltdiv2  8609  lediv2  8613  lbinfle  8672  xrletr  9546  xrre2  9559  xaddass  9607  ixxdisj  9641  ubioc1  9667  lbico1  9668  elioo5  9671  iccsupr  9704  lbicc2  9722  ubicc2  9723  iccneg  9727  icoshft  9728  icodisj  9730  iccf1o  9742  zltaddlt1le  9744  fztri3or  9774  fzdcel  9775  fzen  9778  uzsubsubfz  9782  fzrevral2  9841  fzshftral  9843  fz0fzdiffz0  9862  difelfznle  9867  fzo1fzo0n0  9915  fzonmapblen  9919  fzosubel2  9927  ubmelfzo  9932  elfzodifsumelfzo  9933  ssfzo12bi  9957  ubmelm1fzo  9958  subfzo0  9974  ceiqle  10041  modqid2  10079  zmodidfzoimp  10082  addmodidr  10101  modfzo0difsn  10123  addmodlteq  10126  frec2uzf1od  10134  exprecap  10289  expdivap  10299  expubnd  10305  sqdivap  10312  mulbinom2  10363  bernneq2  10368  bcval3  10452  bccmpl  10455  omgadd  10503  shftval2  10553  mulreap  10591  elicc4abs  10821  abssubge0  10829  abssuble0  10830  maxleast  10940  maxltsup  10945  xrmaxltsup  10982  xrmineqinf  10993  xrltmininf  10994  xrlemininf  10995  fsumdifsnconst  11179  sin01gt0  11382  cos01gt0  11383  sin02gt0  11384  dvdscmul  11432  summodnegmod  11436  modmulconst  11437  dvdsleabs  11455  dvdsleabs2  11456  addmodlteqALT  11469  dvdsexp  11471  mulmoddvds  11473  divalgb  11534  divgcdz  11572  gcdass  11615  mulgcdr  11618  gcddiv  11619  lcmass  11678  coprmdvds  11685  qredeq  11689  qredeu  11690  congr  11693  divgcdcoprm0  11694  divgcdcoprmex  11695  cncongr1  11696  cncongr2  11697  isprm3  11711  dvdsnprmd  11718  euclemma  11736  prmdvdsexpb  11739  prmexpb  11741  rpexp  11743  znege1  11767  strle3g  11962  basgen  12160  clsss  12198  ntrin  12204  ntrcls0  12211  neiint  12225  neiss  12230  neipsm  12234  opnssneib  12236  innei  12243  restco  12254  iscnp  12279  cnconst2  12313  txcn  12355  psmetsym  12409  psmetlecl  12414  distspace  12415  xmetlecl  12447  xmetsym  12448  xblcntrps  12493  xblcntr  12494  blssec  12518  blpnfctr  12519  txmetcn  12599  cnmet  12610  dvid  12742  ptolemy  12816  sinq12gt0  12822
  Copyright terms: Public domain W3C validator