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

Theorem 3adant1 921
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 902 . 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  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  3ad2ant2  925  3ad2ant3  926  rsp2e  2366  sbciegft  2787  reuhyp  4170  suc11g  4235  soinxp  4353  breldmg  4484  funopg  4877  funimaexglem  4925  fex2  5002  fnreseql  5220  ftpg  5290  mpt2eq3ia  5512  mpt2fvex  5771  poxp  5794  smores3  5849  tfrlemibxssdm  5882  nndi  6004  nnmass  6005  nndir  6008  nnaord  6018  nnaordr  6019  nnawordi  6024  nnmord  6026  ecopovtrn  6139  ecopovtrng  6142  ltsopi  6304  addassnqg  6366  ltsonq  6382  ltmnqg  6385  distrnq0  6441  addlocpr  6519  distrlem1prl  6556  distrlem1pru  6557  distrlem4prl  6558  distrlem4pru  6559  ltpopr  6567  ltsopr  6568  addcanprg  6588  lttrsr  6650  ltsosr  6652  ltasrg  6658  recexgt0sr  6661  mulextsr1lem  6666  mulextsr1  6667  axpre-mulext  6732  adddir  6776  axltwlin  6844  axlttrn  6845  ltleletr  6857  letr  6858  mul32  6900  mul31  6901  add32  6927  subsub23  6973  addsubass  6978  subcan2  6992  subsub2  6995  nppcan2  6998  sub32  7001  nnncan  7002  nnncan2  7004  pnpcan2  7007  subdi  7138  subdir  7139  reapcotr  7342  receuap  7392  divmulap3  7398  divrecap  7409  divrecap2  7410  divsubdirap  7426  divdivap1  7441  redivclap  7449  div2negap  7453  ltmul2  7563  lemul2  7564  lemul2a  7566  lediv1  7576  gt0div  7577  ge0div  7578  ltdivmul  7583  ltdivmul2  7585  ledivmul2  7587  uzind2  8086  nn0ind  8088  fnn0ind  8090  uz3m2nn  8251  xrletr  8454  xrre2  8464  ixxdisj  8502  iooneg  8586  iccneg  8587  icoshft  8588  icoshftf1o  8589  icodisj  8590  fzen  8637  fzrev3  8679  2ffzeq  8728  fzoaddel2  8779  elfzodifsumelfzo  8787  ssfzo12bi  8811  fzoshftral  8824  frec2uzf1od  8833  expdivap  8919  mulreap  9052  bj-peano4  9343
  Copyright terms: Public domain W3C validator