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

Theorem 3adant1 957
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 938 . 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:  3ad2ant2  961  3ad2ant3  962  rsp2e  2420  sbciegft  2854  reuhyp  4251  suc11g  4329  soinxp  4457  breldmg  4590  funopg  4985  funimaexglem  5034  fex2  5111  fnreseql  5331  ftpg  5401  mpt2eq3ia  5623  mpt2fvex  5882  poxp  5906  smores3  5964  tfrlemibxssdm  5998  nndi  6152  nnmass  6153  nndir  6156  nnaord  6171  nnaordr  6172  nnawordi  6177  nnmord  6179  ecopovtrn  6292  ecopovtrng  6295  ltsopi  6649  addassnqg  6711  ltsonq  6727  ltmnqg  6730  distrnq0  6788  addlocpr  6865  distrlem1prl  6911  distrlem1pru  6912  distrlem4prl  6913  distrlem4pru  6914  ltpopr  6924  ltsopr  6925  addcanprg  6945  lttrsr  7078  ltsosr  7080  ltasrg  7086  recexgt0sr  7089  mulextsr1lem  7095  mulextsr1  7096  axpre-mulext  7193  adddir  7249  axltwlin  7324  axlttrn  7325  ltleletr  7337  letr  7338  mul32  7382  mul31  7383  add32  7411  subsub23  7457  addsubass  7462  subcan2  7477  subsub2  7480  nppcan2  7483  sub32  7486  nnncan  7487  nnncan2  7489  pnpcan2  7492  subdi  7633  subdir  7634  reapcotr  7842  receuap  7903  divmulap3  7909  divrecap  7920  divrecap2  7921  divsubdirap  7940  divdivap1  7955  redivclap  7963  div2negap  7967  ltmul2  8078  lemul2  8079  lemul2a  8081  lediv1  8091  gt0div  8092  ge0div  8093  ltdivmul  8098  ltdivmul2  8100  ledivmul2  8102  uzind2  8617  nn0ind  8619  fnn0ind  8621  uz3m2nn  8819  xrletr  9031  xrre2  9041  ixxdisj  9079  iooneg  9163  iccneg  9164  icoshft  9165  icoshftf1o  9166  icodisj  9167  fzen  9215  fzrev3  9257  2ffzeq  9305  fzoaddel2  9356  elfzodifsumelfzo  9364  ssfzo12bi  9388  fzoshftral  9401  adddivflid  9451  fldiv4p1lem1div2  9464  modqmulnn  9501  modqeqmodmin  9553  frec2uzf1od  9565  expdivap  9701  shftval2  9940  mulreap  9977  absdivap  10182  absdiflt  10204  absdifle  10205  abs3dif  10217  cau3  10227  ltmininf  10342  dvdsmulc  10456  dvdsmultr1  10466  dvdsmultr2  10468  dvdssub2  10470  oexpneg  10509  divalgb  10557  ndvdsadd  10563  gcdaddm  10607  modgcd  10614  dvdsgcd  10633  dvdsgcdb  10634  gcdass  10636  mulgcd  10637  absmulgcd  10638  rpmulgcd  10647  nn0seqcvgd  10655  ialgcvga  10665  lcmdvds  10693  lcmdvdsb  10698  lcmass  10699  coprmdvds  10706  coprmdvds2  10707  rpmul  10712  cncongr1  10717  cncongr2  10718  prmgt1  10745  qnumdenbi  10802  bj-peano4  11042
  Copyright terms: Public domain W3C validator