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

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

Proof of Theorem 3adant1
StepHypRef Expression
1 3simpc 903 . 2 ((𝜃𝜑𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 14 1 ((𝜃𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  3ad2ant2  926  3ad2ant3  927  rsp2e  2372  sbciegft  2793  reuhyp  4204  suc11g  4281  soinxp  4410  breldmg  4541  funopg  4934  funimaexglem  4982  fex2  5059  fnreseql  5277  ftpg  5347  mpt2eq3ia  5570  mpt2fvex  5829  poxp  5853  smores3  5908  tfrlemibxssdm  5941  nndi  6065  nnmass  6066  nndir  6069  nnaord  6082  nnaordr  6083  nnawordi  6088  nnmord  6090  ecopovtrn  6203  ecopovtrng  6206  ltsopi  6416  addassnqg  6478  ltsonq  6494  ltmnqg  6497  distrnq0  6555  addlocpr  6632  distrlem1prl  6678  distrlem1pru  6679  distrlem4prl  6680  distrlem4pru  6681  ltpopr  6691  ltsopr  6692  addcanprg  6712  lttrsr  6845  ltsosr  6847  ltasrg  6853  recexgt0sr  6856  mulextsr1lem  6862  mulextsr1  6863  axpre-mulext  6960  adddir  7016  axltwlin  7085  axlttrn  7086  ltleletr  7098  letr  7099  mul32  7141  mul31  7142  add32  7168  subsub23  7214  addsubass  7219  subcan2  7234  subsub2  7237  nppcan2  7240  sub32  7243  nnncan  7244  nnncan2  7246  pnpcan2  7249  subdi  7380  subdir  7381  reapcotr  7587  receuap  7648  divmulap3  7654  divrecap  7665  divrecap2  7666  divsubdirap  7682  divdivap1  7697  redivclap  7705  div2negap  7709  ltmul2  7820  lemul2  7821  lemul2a  7823  lediv1  7833  gt0div  7834  ge0div  7835  ltdivmul  7840  ltdivmul2  7842  ledivmul2  7844  uzind2  8348  nn0ind  8350  fnn0ind  8352  uz3m2nn  8513  xrletr  8722  xrre2  8732  ixxdisj  8770  iooneg  8854  iccneg  8855  icoshft  8856  icoshftf1o  8857  icodisj  8858  fzen  8905  fzrev3  8947  2ffzeq  8996  fzoaddel2  9047  elfzodifsumelfzo  9055  ssfzo12bi  9079  fzoshftral  9092  adddivflid  9132  fldiv4p1lem1div2  9145  modqmulnn  9182  frec2uzf1od  9190  expdivap  9303  shftval2  9425  mulreap  9462  absdivap  9666  absdiflt  9686  absdifle  9687  abs3dif  9699  cau3  9709  nn0seqcvgd  9878  ialgcvga  9888  bj-peano4  10078
  Copyright terms: Public domain W3C validator