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

Theorem 3adant3 912
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 889 . 2 ((φ ψ θ) → (φ ψ))
2 3adant.1 . 2 ((φ ψ) → χ)
31, 2syl 14 1 ((φ ψ θ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 873
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 875
This theorem is referenced by:  vtoclgft  2581  eqeu  2688  tpssi  3504  issod  4030  sotricim  4034  soinxp  4337  funopg  4860  fnco  4933  resasplitss  4994  resdif  5073  fnimapr  5158  ftpg  5272  fsnunfv  5288  fvpr1g  5292  fvpr2g  5293  f1ocnvfvb  5345  f1oiso2  5391  moriotass  5420  f1ofveu  5424  acexmid  5435  ovig  5545  ov6g  5561  ovg  5562  ot1stg  5702  ot2ndg  5703  poxp  5775  brtposg  5791  smores3  5830  smoiso  5839  rdgivallem  5888  frecsuclemdm  5904  frecsuclem3  5906  nnaord  5993  nnaword  5995  nnawordex  6012  ecopovtrn  6114  ecopovtrng  6117  ltsopi  6180  addcanpig  6194  distrnqg  6246  ltsonq  6257  ltanqg  6259  ltmnqg  6260  nnanq0  6313  distrnq0  6314  distnq0r  6318  prarloclem  6355  genpassl  6379  genpassu  6380  distrlem1prl  6421  distrlem1pru  6422  distrlem5prl  6425  distrlem5pru  6426  1idprl  6429  1idpru  6430  ltpopr  6432  ltsopr  6433  ltexprlemm  6437  ltexprlemfl  6446  ltexprlemfu  6448  addcanprleml  6451  addcanprlemu  6452  recexprlem1ssl  6467  recexprlem1ssu  6468  lttrsr  6509  ltsosr  6511  ltasrg  6517  recexsrlem  6520  axmulass  6567  ltxrlt  6686  axltwlin  6688  axlttrn  6689  axltadd  6690  letr  6699  mul12  6729  add12  6756  subadd  6801  addsub  6809  npncan  6818  nppcan  6819  nnpcan  6820  nppcan3  6821  pnpcan  6836  pnncan  6838  ppncan  6839  subdi  6968
  Copyright terms: Public domain W3C validator