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

Theorem ad2ant2r 478
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1 ((φ ψ) → χ)
Assertion
Ref Expression
ad2ant2r (((φ θ) (ψ τ)) → χ)

Proof of Theorem ad2ant2r
StepHypRef Expression
1 ad2ant2.1 . . 3 ((φ ψ) → χ)
21adantrr 448 . 2 ((φ (ψ τ)) → χ)
32adantlr 446 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:  foco  5059  fliftfun  5379  f1imaen2g  6209  mulcomnqg  6367  mulassnqg  6368  ltdcnq  6381  lt2addnq  6388  enq0ref  6415  enq0tr  6416  addcmpblnq0  6425  nqpnq0nq  6435  nqnq0m  6437  mulcomnq0  6442  addlocpr  6518  nqprl  6532  prmuloc  6546  distrlem1prl  6557  distrlem1pru  6558  ltaddpr  6570  ltexprlemopu  6576  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  addcomsrg  6663  mulcomsrg  6665  mulasssrg  6666  distrsrg  6667  addcnsr  6711  mulcnsr  6712  addcnsrec  6719  axaddcl  6730  axaddcom  6734  addsub4  7030  muladd  7157  mullt0  7250  apreim  7367  mulge0  7383  divmuldivap  7450  divmul24ap  7454  divmuleqap  7455  recdivap  7456  divadddivap  7465  conjmulap  7467  prodgt0gt0  7578  ltmul12a  7587  lemul12b  7588  lediv2a  7622  qmulcl  8328  irrmul  8336  xrrege0  8488  ge0addcl  8600  ge0mulcl  8601  fzass4  8675  fzrev  8696  fzocatel  8805  expclzaplem  8913  expge0  8925  expge1  8926  lt2sq  8960  le2sq  8961  bernneq  9002
  Copyright terms: Public domain W3C validator