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

Theorem 3adant3 923
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 900 . 2 ((φ ψ θ) → (φ ψ))
2 3adant.1 . 2 ((φ ψ) → χ)
31, 2syl 14 1 ((φ ψ θ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
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 886
This theorem is referenced by:  stoic4a  1318  stoic4b  1319  vtoclgft  2598  eqeu  2705  tpssi  3521  issod  4047  sotricim  4051  soinxp  4353  funopg  4877  fnco  4950  resasplitss  5012  resdif  5091  fnimapr  5176  ftpg  5290  fsnunfv  5306  fvpr1g  5310  fvpr2g  5311  f1ocnvfvb  5363  f1oiso2  5409  moriotass  5439  f1ofveu  5443  acexmid  5454  ovig  5564  ov6g  5580  ovg  5581  ot1stg  5721  ot2ndg  5722  poxp  5794  brtposg  5810  smores3  5849  smoiso  5858  rdgivallem  5908  frecsuclemdm  5927  frecsuclem3  5929  nnaord  6018  nnaword  6020  nnawordex  6037  ecopovtrn  6139  ecopovtrng  6142  xpdom3m  6244  ltsopi  6304  addcanpig  6318  distrnqg  6371  ltsonq  6382  ltanqg  6384  ltmnqg  6385  nnanq0  6440  distrnq0  6441  distnq0r  6445  prarloclem  6483  genpassl  6507  genpassu  6508  distrlem1prl  6556  distrlem1pru  6557  distrlem5prl  6560  distrlem5pru  6561  1idprl  6564  1idpru  6565  ltpopr  6567  ltsopr  6568  ltexprlemm  6572  ltexprlemfl  6581  ltexprlemfu  6583  addcanprlemu  6587  recexprlem1ssl  6603  recexprlem1ssu  6604  aptipr  6611  lttrsr  6650  ltsosr  6652  ltasrg  6658  recexgt0sr  6661  mulextsr1  6667  axmulass  6717  ltxrlt  6842  axltwlin  6844  axlttrn  6845  axltadd  6846  letr  6858  mul12  6899  add12  6926  subadd  6971  addsub  6979  npncan  6988  nppcan  6989  nnpcan  6990  nppcan3  6991  pnpcan  7006  pnncan  7008  ppncan  7009  subdi  7138  ltaddsub2  7187  leaddsub2  7189  ltaddsublt  7315  apreap  7331  lemul1  7337  reapmul1lem  7338  reapadd1  7340  reapcotr  7342  receuap  7392  divassap  7411  div23ap  7412  divcanap4  7418  divsubdirap  7426  divcanap5  7432  divdiv32ap  7438  divdivap2  7442  letrp1  7555  ltmulgt12  7572  lediv1  7576  ltdiv2  7594  lediv2  7598  xrletr  8454  xrre2  8464  ixxdisj  8502  ubioc1  8528  lbico1  8529  elioo5  8532  iccsupr  8565  lbicc2  8582  ubicc2  8583  iccneg  8587  icoshft  8588  icodisj  8590  iccf1o  8602  fztri3or  8633  fzdcel  8634  fzen  8637  uzsubsubfz  8641  fzrevral2  8698  fzshftral  8700  fz0fzdiffz0  8717  elfzmlbmOLD  8719  difelfznle  8723  fzo1fzo0n0  8769  fzonmapblen  8773  fzosubel2  8781  ubmelfzo  8786  elfzodifsumelfzo  8787  ssfzo12bi  8811  ubmelm1fzo  8812  frec2uzf1od  8833  exprecap  8910  expdivap  8919  expubnd  8925  sqdivap  8932  bernneq2  8983  mulreap  9052
  Copyright terms: Public domain W3C validator