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

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

Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 901 . 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
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  stoic4a  1321  stoic4b  1322  vtoclgft  2604  eqeu  2711  tpssi  3530  issod  4056  sotricim  4060  soinxp  4410  funopg  4934  fnco  5007  resasplitss  5069  resdif  5148  fnimapr  5233  ftpg  5347  fsnunfv  5363  fvpr1g  5367  fvpr2g  5368  f1ocnvfvb  5420  f1oiso2  5466  moriotass  5496  f1ofveu  5500  acexmid  5511  ovig  5622  ov6g  5638  ovg  5639  ot1stg  5779  ot2ndg  5780  poxp  5853  brtposg  5869  smores3  5908  smoiso  5917  rdgivallem  5968  frecsuclemdm  5988  frecsuclem3  5990  nnaord  6082  nnaword  6084  nnawordex  6101  ecopovtrn  6203  ecopovtrng  6206  xpdom3m  6308  ltsopi  6416  addcanpig  6430  distrnqg  6483  ltsonq  6494  ltanqg  6496  ltmnqg  6497  nnanq0  6554  distrnq0  6555  distnq0r  6559  prarloclem  6597  genpassl  6620  genpassu  6621  distrlem1prl  6678  distrlem1pru  6679  distrlem5prl  6682  distrlem5pru  6683  1idprl  6686  1idpru  6687  ltpopr  6691  ltsopr  6692  ltexprlemm  6696  ltexprlemfl  6705  ltexprlemfu  6707  addcanprlemu  6711  recexprlem1ssl  6729  recexprlem1ssu  6730  aptipr  6737  lttrsr  6845  ltsosr  6847  ltasrg  6853  recexgt0sr  6856  mulextsr1  6863  axmulass  6945  ltxrlt  7083  axltwlin  7085  axlttrn  7086  axltadd  7087  letr  7099  mul12  7140  add12  7167  subadd  7212  addsub  7220  npncan  7230  nppcan  7231  nnpcan  7232  nppcan3  7233  pnpcan  7248  pnncan  7250  ppncan  7251  subdi  7380  ltaddsub2  7430  leaddsub2  7432  ltaddsublt  7560  apreap  7576  lemul1  7582  reapmul1lem  7583  reapadd1  7585  reapcotr  7587  receuap  7648  divassap  7667  div23ap  7668  divcanap4  7674  divsubdirap  7682  divcanap5  7688  divdiv32ap  7694  divdivap2  7698  letrp1  7812  ltmulgt12  7829  lediv1  7833  ltdiv2  7851  lediv2  7855  xrletr  8722  xrre2  8732  ixxdisj  8770  ubioc1  8796  lbico1  8797  elioo5  8800  iccsupr  8833  lbicc2  8850  ubicc2  8851  iccneg  8855  icoshft  8856  icodisj  8858  iccf1o  8870  fztri3or  8901  fzdcel  8902  fzen  8905  uzsubsubfz  8909  fzrevral2  8966  fzshftral  8968  fz0fzdiffz0  8985  elfzmlbmOLD  8987  difelfznle  8991  fzo1fzo0n0  9037  fzonmapblen  9041  fzosubel2  9049  ubmelfzo  9054  elfzodifsumelfzo  9055  ssfzo12bi  9079  ubmelm1fzo  9080  subfzo0  9095  ceiqle  9153  frec2uzf1od  9166  exprecap  9270  expdivap  9279  expubnd  9285  sqdivap  9292  bernneq2  9344  shftval2  9401  mulreap  9438  elicc4abs  9664  abssubge0  9672  abssuble0  9673
  Copyright terms: Public domain W3C validator