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

Theorem 3adant2 960
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 939 . 2 ((𝜑𝜃𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
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 924
This theorem is referenced by:  3ad2ant1  962  eupickb  2026  vtoclegft  2684  eqeu  2776  suc11g  4345  soinxp  4475  funopg  5010  fnco  5084  dff1o2  5215  fnimapr  5321  fvun1  5327  fvmptt  5351  fnreseql  5366  fvpr1g  5458  fvpr2g  5459  f1elima  5507  f1ocnvfvb  5514  ovexg  5634  oprssov  5737  poxp  5948  smoiso  6015  rdgivallem  6094  nndi  6195  nndir  6199  nnaord  6214  nnaordr  6215  nnaword  6216  nnawordi  6220  ecopovtrn  6335  ecopovtrng  6338  xpdom3m  6496  mapxpen  6510  findcard  6550  fisseneq  6586  resfnfinfinss  6593  funrnfi  6595  ltsopi  6816  addcanpig  6830  addassnqg  6878  distrnqg  6883  ltsonq  6894  ltmnqg  6897  prarloclemarch2  6915  nnanq0  6954  distrnq0  6955  distnq0r  6959  prltlu  6983  prarloclem5  6996  distrlem1prl  7078  distrlem1pru  7079  distrlem5prl  7082  distrlem5pru  7083  ltpopr  7091  ltsopr  7092  ltexprlemm  7096  ltexprlemfl  7105  ltexprlemfu  7107  lttrsr  7245  ltsosr  7247  ltasrg  7253  recexgt0sr  7256  mulextsr1lem  7262  mulextsr1  7263  axpre-mulext  7360  adddir  7416  axltwlin  7491  axlttrn  7492  ltleletr  7504  letr  7505  nnncan1  7655  npncan3  7657  pnpcan2  7659  subdi  7800  subdir  7801  reapcotr  8009  divmulap  8074  div23ap  8090  div13ap  8092  muldivdirap  8106  divsubdirap  8107  divcanap7  8120  ltmul2  8245  lemul2  8246  lemul2a  8248  lediv1  8258  ltmuldiv2  8264  lemuldiv2  8271  squeeze0  8293  nndivtr  8391  bndndx  8598  nn0n0n1ge2  8743  fnn0ind  8788  addlelt  9164  xrletr  9198  xrltne  9203  iooneg  9330  iccneg  9331  icoshft  9332  icoshftf1o  9333  zltaddlt1le  9348  fztri3or  9378  fzdcel  9379  fzen  9382  uzsubsubfz  9386  fzrevral2  9443  fzshftral  9445  fz0fzdiffz0  9462  elfzmlbp  9464  elfzo  9481  fzoaddel2  9525  fzosubel2  9527  elfzom1p1elfzo  9546  ssfzo12bi  9557  subfzo0  9574  flltdivnn0lt  9632  modqmulnn  9670  modfzo0difsn  9723  expdivap  9897  expubnd  9903  mulbinom2  9959  bernneq2  9964  shftuz  10140  shftval2  10149  abs3dif  10426  dvdsval2  10666  dvdscmul  10690  dvdsmulc  10691  ndvdssub  10797  rpmulgcd  10882  cncongr1  10952  cncongr2  10953  isprm3  10967  bj-peano4  11280
  Copyright terms: Public domain W3C validator