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

Theorem 3adant3 1001
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 978 . 2 ((𝜑𝜓𝜃) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962
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 964
This theorem is referenced by:  stoic4a  1408  stoic4b  1409  vtoclgft  2736  eqeu  2854  tpssi  3689  issod  4244  sotricim  4248  soinxp  4612  funopg  5160  fnco  5234  resasplitss  5305  resdif  5392  fnimapr  5484  ftpg  5607  fsnunfv  5624  fvpr1g  5629  fvpr2g  5630  f1ocnvfvb  5684  f1oiso2  5731  moriotass  5761  f1ofveu  5765  acexmid  5776  ovig  5895  ov6g  5911  ovg  5912  ot1stg  6053  ot2ndg  6054  poxp  6132  brtposg  6154  smores3  6193  smoiso  6202  rdgivallem  6281  frecsuclem  6306  nnaord  6408  nnaword  6410  nnawordex  6427  ecopovtrn  6529  ecopovtrng  6532  xpdom3m  6731  mapxpen  6745  sbthlemi4  6851  djuenun  7080  ltsopi  7147  addcanpig  7161  distrnqg  7214  ltsonq  7225  ltanqg  7227  ltmnqg  7228  nnanq0  7285  distrnq0  7286  distnq0r  7290  prarloclem  7328  genpassl  7351  genpassu  7352  distrlem1prl  7409  distrlem1pru  7410  distrlem5prl  7413  distrlem5pru  7414  1idprl  7417  1idpru  7418  ltpopr  7422  ltsopr  7423  ltexprlemm  7427  ltexprlemfl  7436  ltexprlemfu  7438  addcanprlemu  7442  recexprlem1ssl  7460  recexprlem1ssu  7461  aptipr  7468  lttrsr  7589  ltsosr  7591  ltasrg  7597  recexgt0sr  7600  mulextsr1  7608  axmulass  7700  ltxrlt  7849  axltwlin  7851  axlttrn  7852  axltadd  7853  letr  7866  mul12  7910  add12  7939  subadd  7984  addsub  7992  npncan  8002  nppcan  8003  nnpcan  8004  nppcan3  8005  pnpcan  8020  pnncan  8022  ppncan  8023  subdi  8166  ltaddsub2  8218  leaddsub2  8220  ltaddsublt  8352  apreap  8368  lemul1  8374  reapmul1lem  8375  reapadd1  8377  reapcotr  8379  receuap  8449  divassap  8469  div23ap  8470  divmulassap  8474  divmulasscomap  8475  divcanap4  8478  divsubdirap  8487  divcanap5  8493  divdiv32ap  8499  divdivap2  8503  div2subap  8615  letrp1  8625  ltmulgt12  8642  lediv1  8646  ltdiv2  8664  lediv2  8668  lbinfle  8727  xrletr  9614  xrre2  9627  xaddass  9675  ixxdisj  9709  ubioc1  9735  lbico1  9736  elioo5  9739  iccsupr  9772  lbicc2  9790  ubicc2  9791  iccneg  9795  icoshft  9796  icodisj  9798  iccf1o  9810  iccen  9812  zltaddlt1le  9813  fztri3or  9843  fzdcel  9844  fzen  9847  uzsubsubfz  9851  fzrevral2  9910  fzshftral  9912  fz0fzdiffz0  9931  difelfznle  9936  fzo1fzo0n0  9984  fzonmapblen  9988  fzosubel2  9996  ubmelfzo  10001  elfzodifsumelfzo  10002  ssfzo12bi  10026  ubmelm1fzo  10027  subfzo0  10043  ceiqle  10110  modqid2  10148  zmodidfzoimp  10151  addmodidr  10170  modfzo0difsn  10192  addmodlteq  10195  frec2uzf1od  10203  exprecap  10358  expdivap  10368  expubnd  10374  sqdivap  10381  mulbinom2  10432  bernneq2  10437  bcval3  10521  bccmpl  10524  omgadd  10572  shftval2  10622  mulreap  10660  elicc4abs  10890  abssubge0  10898  abssuble0  10899  maxleast  11009  maxltsup  11014  xrmaxltsup  11051  xrmineqinf  11062  xrltmininf  11063  xrlemininf  11064  fsumdifsnconst  11248  prodfap0  11338  prodfrecap  11339  sin01gt0  11491  cos01gt0  11492  sin02gt0  11493  dvdscmul  11543  summodnegmod  11547  modmulconst  11548  dvdsleabs  11566  dvdsleabs2  11567  addmodlteqALT  11580  dvdsexp  11582  mulmoddvds  11584  divalgb  11645  divgcdz  11683  gcdass  11726  mulgcdr  11729  gcddiv  11730  lcmass  11789  coprmdvds  11796  qredeq  11800  qredeu  11801  congr  11804  divgcdcoprm0  11805  divgcdcoprmex  11806  cncongr1  11807  cncongr2  11808  isprm3  11822  dvdsnprmd  11829  euclemma  11847  prmdvdsexpb  11850  prmexpb  11852  rpexp  11854  znege1  11879  strle3g  12077  basgen  12275  clsss  12313  ntrin  12319  ntrcls0  12326  neiint  12340  neiss  12345  neipsm  12349  opnssneib  12351  innei  12358  restco  12369  iscnp  12394  cnconst2  12428  txcn  12470  psmetsym  12524  psmetlecl  12529  distspace  12530  xmetlecl  12562  xmetsym  12563  xblcntrps  12608  xblcntr  12609  blssec  12633  blpnfctr  12634  txmetcn  12714  cnmet  12725  dvid  12857  ptolemy  12939  sinq12gt0  12945  sincosq1eq  12954  rpcxpsub  13023  relogbexpap  13068  logbleb  13071  logblt  13072  rplogbcxp  13073
  Copyright terms: Public domain W3C validator