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

Theorem 3ad2antl2 1222
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 750 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl1 1215 1 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  fcofo  6528  cocan1  6531  ordiso2  8405  fin1a2lem9  9215  fin1a2lem12  9218  gchpwdom  9477  winainflem  9500  bpolydif  14767  muldvds1  14987  lcmdvds  15302  ramcl  15714  gsumccat  17359  oddvdsnn0  17944  ghmplusg  18230  frlmsslss2  20095  frlmsslsp  20116  islindf4  20158  mamures  20177  matepmcl  20249  matepm2cl  20250  pmatcollpw2lem  20563  cnpnei  21049  ssref  21296  qtopss  21499  elfm2  21733  flffbas  21780  cnpfcf  21826  deg1ldg  23833  brbtwn2  25766  colinearalg  25771  axsegconlem1  25778  upgrpredgv  26015  cusgrrusgr  26458  upgrewlkle2  26483  wwlksm1edg  26748  clwwlksf  26895  nvmul0or  27475  hoadddi  28632  volfiniune  30267  bnj548  30941  funsseq  31642  nn0prpwlem  32292  fnemeet1  32336  curfv  33360  keridl  33802  pmapglbx  34874  elpaddn0  34905  paddasslem9  34933  paddasslem10  34934  cdleme42mgN  35595  relexpxpmin  37828  ntrclsk3  38188  n0p  39029  wessf1ornlem  39187  infxr  39396  lptre2pt  39672  dvnprodlem1  39924  fourierdlem42  40129  fourierdlem48  40134  fourierdlem54  40140  fourierdlem77  40163  sge0rpcpnf  40401  hoicvr  40525  smflimsuplem7  40795
  Copyright terms: Public domain W3C validator