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

Theorem ad2ant2r 493
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 463 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantlr 461 1 (((𝜑𝜃) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  foco  5206  fvco4  5339  fliftfun  5536  f1imaen2g  6462  fodjuomnilem0  6746  mulcomnqg  6886  mulassnqg  6887  ltdcnq  6900  lt2addnq  6907  lt2mulnq  6908  enq0ref  6936  enq0tr  6937  addcmpblnq0  6946  nqpnq0nq  6956  nqnq0m  6958  mulcomnq0  6963  addlocpr  7039  nqprl  7054  nqpru  7055  prmuloc  7069  distrlem1prl  7085  distrlem1pru  7086  ltaddpr  7100  ltexprlemopu  7106  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemrl  7113  ltexprlemru  7115  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  caucvgprprlemopu  7202  addcomsrg  7245  mulcomsrg  7247  mulasssrg  7248  distrsrg  7249  addcnsr  7315  mulcnsr  7316  addcnsrec  7323  axaddcl  7345  axaddcom  7349  addsub4  7669  muladd  7806  mullt0  7902  apreim  8021  mulge0  8037  divmuldivap  8118  divmul24ap  8122  divmuleqap  8123  recdivap  8124  divadddivap  8133  conjmulap  8135  prodgt0gt0  8247  ltmul12a  8256  lemul12b  8257  lediv2a  8291  qmulcl  9054  irrmul  9064  xrrege0  9219  ge0addcl  9331  ge0mulcl  9332  fzass4  9407  fzrev  9428  fzocatel  9538  serige0  9850  expclzaplem  9877  expge0  9889  expge1  9890  lt2sq  9926  le2sq  9927  bernneq  9970  sq11ap  10016  sqrt11ap  10366  2clim  10582  climge0  10605  opeo  10772  omeo  10773  cncongr1  10960
  Copyright terms: Public domain W3C validator