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

Theorem 3adant2 985
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 964 . 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  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  3ad2ant1  987  eupickb  2058  vtoclegft  2732  eqeu  2827  suc11g  4442  soinxp  4579  funopg  5127  fnco  5201  dff1o2  5340  fnimapr  5449  fvun1  5455  fvmptt  5480  fnreseql  5498  fvpr1g  5594  fvpr2g  5595  f1elima  5642  f1ocnvfvb  5649  ovexg  5773  oprssov  5880  poxp  6097  smoiso  6167  rdgivallem  6246  nndi  6350  nndir  6354  fnsnsplitdc  6369  nnaord  6373  nnaordr  6374  nnaword  6375  nnawordi  6379  ecopovtrn  6494  ecopovtrng  6497  xpdom3m  6696  mapxpen  6710  findcard  6750  fisseneq  6788  resfnfinfinss  6796  funrnfi  6798  ltsopi  7096  addcanpig  7110  addassnqg  7158  distrnqg  7163  ltsonq  7174  ltmnqg  7177  prarloclemarch2  7195  nnanq0  7234  distrnq0  7235  distnq0r  7239  prltlu  7263  prarloclem5  7276  distrlem1prl  7358  distrlem1pru  7359  distrlem5prl  7362  distrlem5pru  7363  ltpopr  7371  ltsopr  7372  ltexprlemm  7376  ltexprlemfl  7385  ltexprlemfu  7387  lttrsr  7538  ltsosr  7540  ltasrg  7546  recexgt0sr  7549  mulextsr1lem  7556  mulextsr1  7557  axpre-mulext  7664  adddir  7725  axltwlin  7800  axlttrn  7801  ltleletr  7814  letr  7815  nnncan1  7966  npncan3  7968  pnpcan2  7970  subdi  8115  subdir  8116  reapcotr  8328  divmulap  8403  div23ap  8419  div13ap  8421  muldivdirap  8435  divsubdirap  8436  divcanap7  8449  ltmul2  8582  lemul2  8583  lemul2a  8585  lediv1  8595  ltmuldiv2  8601  lemuldiv2  8608  squeeze0  8630  nndivtr  8730  bndndx  8944  nn0n0n1ge2  9089  fnn0ind  9135  addlelt  9523  xrletr  9559  xrltne  9564  xleadd2a  9625  xleadd1  9626  xltadd2  9628  iooneg  9739  iccneg  9740  icoshft  9741  icoshftf1o  9742  zltaddlt1le  9757  fztri3or  9787  fzdcel  9788  fzen  9791  uzsubsubfz  9795  fzrevral2  9854  fzshftral  9856  fz0fzdiffz0  9875  elfzmlbp  9877  elfzo  9894  fzoaddel2  9938  fzosubel2  9940  elfzom1p1elfzo  9959  ssfzo12bi  9970  subfzo0  9987  flltdivnn0lt  10045  modqmulnn  10083  modfzo0difsn  10136  expdivap  10312  expubnd  10318  mulbinom2  10376  bernneq2  10381  shftuz  10557  shftval2  10566  abs3dif  10845  xrmaxlesup  10996  xrltmininf  11007  xrlemininf  11008  sin02gt0  11397  dvdsval2  11423  dvdscmul  11447  dvdsmulc  11448  ndvdssub  11554  rpmulgcd  11641  cncongr1  11711  cncongr2  11712  isprm3  11726  ntrin  12220  elnei  12248  cnrest2  12332  psmetsym  12425  psmetge0  12427  xmetge0  12461  xmetsym  12464  cnmet  12626  bj-peano4  13080
  Copyright terms: Public domain W3C validator