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

Theorem ad2ant2l 508
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2l (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)

Proof of Theorem ad2ant2l
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrl 478 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantll 476 1 (((𝜃𝜑) ∧ (𝜏𝜓)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  mpteqb  5602  mpofun  5971  xpdom2  6825  addcmpblnq  7354  addpipqqslem  7356  addpipqqs  7357  addclnq  7362  addcomnqg  7368  addassnqg  7369  mulcomnqg  7370  mulassnqg  7371  distrnqg  7374  ltdcnq  7384  enq0ref  7420  addcmpblnq0  7430  addclnq0  7438  nqpnq0nq  7440  nqnq0a  7441  nqnq0m  7442  distrnq0  7446  mulcomnq0  7447  addassnq0lemcl  7448  genpdisj  7510  appdiv0nq  7551  addcomsrg  7742  mulcomsrg  7744  mulasssrg  7745  distrsrg  7746  addcnsr  7821  mulcnsr  7822  addcnsrec  7829  axaddcl  7851  axmulcl  7853  axaddcom  7857  add42  8106  muladd  8328  mulsub  8345  apreim  8547  divmuleqap  8660  ltmul12a  8803  lemul12b  8804  lemul12a  8805  qaddcl  9621  qmulcl  9623  iooshf  9936  fzass4  10045  elfzomelpfzo  10214  tanaddaplem  11727  opnneissb  13315  neitx  13428  txcnmpt  13433  txrest  13436  metcnp3  13671  cncfmet  13739  dveflem  13847  lgsdir2  14094
  Copyright terms: Public domain W3C validator