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

Theorem adantrr 448
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1 ((φ ψ) → χ)
Assertion
Ref Expression
adantrr ((φ (ψ θ)) → χ)

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 102 . 2 ((ψ θ) → ψ)
2 adant2.1 . 2 ((φ ψ) → χ)
31, 2sylan2 270 1 ((φ (ψ θ)) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
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 is referenced by:  ad2ant2r  478  ad2ant2lr  479  dn1dc  866  3ad2antr1  1068  xordidc  1287  po2nr  4036  sotricim  4050  fmptco  5271  fvtp1g  5310  dff13  5348  fcof1o  5370  isocnv  5392  isores2  5394  isoini  5398  f1oiso2  5407  acexmidlemab  5446  ovmpt2df  5571  offval  5658  xp1st  5731  1stconst  5781  cnvf1olem  5784  mpt2xopoveq  5793  nnaordi  6010  nnmordi  6018  erinxp  6109  dom2lem  6181  fundmen  6215  ltsonq  6375  lt2addnq  6381  ltexnqq  6384  prarloclemarch2  6395  enq0sym  6407  genprndl  6497  genprndu  6498  prmuloc  6537  distrlem1prl  6548  distrlem1pru  6549  ltsopr  6560  ltexprlemdisj  6570  ltexprlemfl  6573  ltexprlemfu  6575  addcanprlemu  6579  ltaprg  6582  mulcmpblnrlemg  6620  recexgt0sr  6653  mul4  6894  2addsub  6974  muladd  7129  ltleadd  7188  divmulap3  7390  divcanap7  7431  divadddivap  7437  lemul2a  7557  lemul12b  7559  ltmuldiv2  7573  ltdivmul  7574  ltdivmul2  7576  ledivmul2  7578  lemuldiv2  7580  lt2msq  7584  cju  7645  zextlt  8057  xrlttr  8434  xrre3  8453  ixxdisj  8490  iooshf  8539  icodisj  8578  iccf1o  8590
  Copyright terms: Public domain W3C validator