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  8301  apreap  8317  lemul1  8323  reapmul1lem  8324  reapadd1  8326  reapcotr  8328  receuap  8398  divassap  8418  div23ap  8419  divmulassap  8423  divmulasscomap  8424  divcanap4  8427  divsubdirap  8436  divcanap5  8442  divdiv32ap  8448  divdivap2  8452  div2subap  8564  letrp1  8574  ltmulgt12  8591  lediv1  8595  ltdiv2  8613  lediv2  8617  lbinfle  8676  xrletr  9559  xrre2  9572  xaddass  9620  ixxdisj  9654  ubioc1  9680  lbico1  9681  elioo5  9684  iccsupr  9717  lbicc2  9735  ubicc2  9736  iccneg  9740  icoshft  9741  icodisj  9743  iccf1o  9755  zltaddlt1le  9757  fztri3or  9787  fzdcel  9788  fzen  9791  uzsubsubfz  9795  fzrevral2  9854  fzshftral  9856  fz0fzdiffz0  9875  difelfznle  9880  fzo1fzo0n0  9928  fzonmapblen  9932  fzosubel2  9940  ubmelfzo  9945  elfzodifsumelfzo  9946  ssfzo12bi  9970  ubmelm1fzo  9971  subfzo0  9987  ceiqle  10054  modqid2  10092  zmodidfzoimp  10095  addmodidr  10114  modfzo0difsn  10136  addmodlteq  10139  frec2uzf1od  10147  exprecap  10302  expdivap  10312  expubnd  10318  sqdivap  10325  mulbinom2  10376  bernneq2  10381  bcval3  10465  bccmpl  10468  omgadd  10516  shftval2  10566  mulreap  10604  elicc4abs  10834  abssubge0  10842  abssuble0  10843  maxleast  10953  maxltsup  10958  xrmaxltsup  10995  xrmineqinf  11006  xrltmininf  11007  xrlemininf  11008  fsumdifsnconst  11192  sin01gt0  11395  cos01gt0  11396  sin02gt0  11397  dvdscmul  11447  summodnegmod  11451  modmulconst  11452  dvdsleabs  11470  dvdsleabs2  11471  addmodlteqALT  11484  dvdsexp  11486  mulmoddvds  11488  divalgb  11549  divgcdz  11587  gcdass  11630  mulgcdr  11633  gcddiv  11634  lcmass  11693  coprmdvds  11700  qredeq  11704  qredeu  11705  congr  11708  divgcdcoprm0  11709  divgcdcoprmex  11710  cncongr1  11711  cncongr2  11712  isprm3  11726  dvdsnprmd  11733  euclemma  11751  prmdvdsexpb  11754  prmexpb  11756  rpexp  11758  znege1  11783  strle3g  11978  basgen  12176  clsss  12214  ntrin  12220  ntrcls0  12227  neiint  12241  neiss  12246  neipsm  12250  opnssneib  12252  innei  12259  restco  12270  iscnp  12295  cnconst2  12329  txcn  12371  psmetsym  12425  psmetlecl  12430  distspace  12431  xmetlecl  12463  xmetsym  12464  xblcntrps  12509  xblcntr  12510  blssec  12534  blpnfctr  12535  txmetcn  12615  cnmet  12626  dvid  12758  ptolemy  12832  sinq12gt0  12838  sincosq1eq  12847
  Copyright terms: Public domain W3C validator