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

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

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 937 . 2 ((𝜑𝜃𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3ad2ant1  960  eupickb  2023  vtoclegft  2671  eqeu  2763  suc11g  4302  soinxp  4430  funopg  4958  fnco  5032  dff1o2  5156  fnimapr  5259  fvun1  5265  fvmptt  5288  fnreseql  5303  fvpr1g  5393  fvpr2g  5394  f1elima  5438  f1ocnvfvb  5445  ovexg  5564  oprssov  5667  poxp  5878  smoiso  5945  rdgivallem  6024  nndi  6123  nndir  6127  nnaord  6141  nnaordr  6142  nnaword  6143  nnawordi  6147  ecopovtrn  6262  ecopovtrng  6265  xpdom3m  6368  findcard  6412  funrnfi  6440  ltsopi  6561  addcanpig  6575  addassnqg  6623  distrnqg  6628  ltsonq  6639  ltmnqg  6642  prarloclemarch2  6660  nnanq0  6699  distrnq0  6700  distnq0r  6704  prltlu  6728  prarloclem5  6741  distrlem1prl  6823  distrlem1pru  6824  distrlem5prl  6827  distrlem5pru  6828  ltpopr  6836  ltsopr  6837  ltexprlemm  6841  ltexprlemfl  6850  ltexprlemfu  6852  lttrsr  6990  ltsosr  6992  ltasrg  6998  recexgt0sr  7001  mulextsr1lem  7007  mulextsr1  7008  axpre-mulext  7105  adddir  7161  axltwlin  7236  axlttrn  7237  ltleletr  7249  letr  7250  nnncan1  7400  npncan3  7402  pnpcan2  7404  subdi  7545  subdir  7546  reapcotr  7754  divmulap  7819  div23ap  7835  div13ap  7837  muldivdirap  7851  divsubdirap  7852  divcanap7  7865  ltmul2  7990  lemul2  7991  lemul2a  7993  lediv1  8003  ltmuldiv2  8009  lemuldiv2  8016  squeeze0  8038  nndivtr  8136  bndndx  8343  nn0n0n1ge2  8488  fnn0ind  8533  addlelt  8909  xrletr  8943  xrltne  8948  iooneg  9075  iccneg  9076  icoshft  9077  icoshftf1o  9078  zltaddlt1le  9093  fztri3or  9123  fzdcel  9124  fzen  9127  uzsubsubfz  9131  fzrevral2  9188  fzshftral  9190  fz0fzdiffz0  9207  elfzmlbp  9209  elfzo  9225  fzoaddel2  9268  fzosubel2  9270  elfzom1p1elfzo  9289  ssfzo12bi  9300  subfzo0  9317  flltdivnn0lt  9375  modqmulnn  9413  modfzo0difsn  9466  expdivap  9613  expubnd  9619  mulbinom2  9675  bernneq2  9680  shftuz  9832  shftval2  9841  abs3dif  10118  dvdsval2  10332  dvdscmul  10356  dvdsmulc  10357  ndvdssub  10463  rpmulgcd  10548  cncongr1  10618  cncongr2  10619  isprm3  10633  bj-peano4  10893
  Copyright terms: Public domain W3C validator