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

Theorem ad2ant2r 486
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 456 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantlr 454 1 (((𝜑𝜃) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  foco  5143  fliftfun  5463  f1imaen2g  6303  mulcomnqg  6538  mulassnqg  6539  ltdcnq  6552  lt2addnq  6559  lt2mulnq  6560  enq0ref  6588  enq0tr  6589  addcmpblnq0  6598  nqpnq0nq  6608  nqnq0m  6610  mulcomnq0  6615  addlocpr  6691  nqprl  6706  nqpru  6707  prmuloc  6721  distrlem1prl  6737  distrlem1pru  6738  ltaddpr  6752  ltexprlemopu  6758  ltexprlemdisj  6761  ltexprlemloc  6762  ltexprlemrl  6765  ltexprlemru  6767  recexprlemloc  6786  recexprlem1ssl  6788  recexprlem1ssu  6789  caucvgprprlemopu  6854  addcomsrg  6897  mulcomsrg  6899  mulasssrg  6900  distrsrg  6901  addcnsr  6967  mulcnsr  6968  addcnsrec  6975  axaddcl  6997  axaddcom  7001  addsub4  7316  muladd  7452  mullt0  7548  apreim  7667  mulge0  7683  divmuldivap  7762  divmul24ap  7766  divmuleqap  7767  recdivap  7768  divadddivap  7777  conjmulap  7779  prodgt0gt0  7891  ltmul12a  7900  lemul12b  7901  lediv2a  7935  qmulcl  8668  irrmul  8678  xrrege0  8838  ge0addcl  8950  ge0mulcl  8951  fzass4  9026  fzrev  9047  fzocatel  9156  serige0  9416  expclzaplem  9443  expge0  9455  expge1  9456  lt2sq  9492  le2sq  9493  bernneq  9536  sq11ap  9582  sqrt11ap  9864  2clim  10052  climge0  10075  opeo  10208  omeo  10209
  Copyright terms: Public domain W3C validator