MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ad2antl2 Structured version   Visualization version   GIF version

Theorem 3ad2antl2 1183
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
3ad2antl2 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl2
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantlr 714 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl1 1163 1 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086
This theorem is referenced by:  simpl2  1189  simpl2l  1223  simpl2r  1224  simpl21  1248  simpl22  1249  simpl23  1250  fcofo  7018  cocan1  7021  ordiso2  8955  fin1a2lem9  9807  fin1a2lem12  9810  gchpwdom  10069  winainflem  10092  bpolydif  15388  dvdsmodexp  15594  muldvds1  15613  lcmdvds  15929  ramcl  16342  gsumccatOLD  17983  oddvdsnn0  18650  ghmplusg  18944  frlmsslss2  20894  frlmsslsp  20915  islindf4  20957  mamures  20976  matepmcl  21046  matepm2cl  21047  pmatcollpw2lem  21360  cnpnei  21847  ssref  22095  qtopss  22298  elfm2  22531  flffbas  22578  cnpfcf  22624  deg1ldg  24671  brbtwn2  26677  colinearalg  26682  axsegconlem1  26689  upgrpredgv  26910  cusgrrusgr  27349  upgrewlkle2  27374  wwlksm1edg  27645  clwwlkf  27810  wwlksext2clwwlk  27820  nvmul0or  28411  hoadddi  29564  volfiniune  31496  bnj548  32176  funsseq  33018  nn0prpwlem  33677  fnemeet1  33721  curfv  34915  lindsadd  34928  keridl  35348  pmapglbx  36943  elpaddn0  36974  paddasslem9  37002  paddasslem10  37003  cdleme42mgN  37662  factwoffsmonot  39212  relexpxpmin  40197  ntrclsk3  40555  n0p  41460  wessf1ornlem  41599  infxr  41789  lptre2pt  42073  dvnprodlem1  42379  fourierdlem42  42582  fourierdlem48  42587  fourierdlem54  42593  fourierdlem77  42616  sge0rpcpnf  42851  hoicvr  42978  smflimsuplem7  43248  isomgrsym  44146
  Copyright terms: Public domain W3C validator