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

Theorem 3ad2antl2 1216
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 746 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl1 1209 1 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  fcofo  6416  cocan1  6419  ordiso2  8275  fin1a2lem9  9085  fin1a2lem12  9088  gchpwdom  9343  winainflem  9366  bpolydif  14566  muldvds1  14785  lcmdvds  15100  ramcl  15512  gsumccat  17142  oddvdsnn0  17727  ghmplusg  18013  frlmsslss2  19870  frlmsslsp  19891  islindf4  19933  mamures  19952  matepmcl  20024  matepm2cl  20025  pmatcollpw2lem  20338  cnpnei  20815  ssref  21062  qtopss  21265  elfm2  21499  flffbas  21546  cnpfcf  21592  deg1ldg  23568  brbtwn2  25498  colinearalg  25503  axsegconlem1  25510  clwwlkf  26083  2spontn0vne  26175  usgreghash2spot  26357  nvmul0or  26672  hoadddi  27847  volfiniune  29421  bnj548  30022  funsseq  30713  nn0prpwlem  31288  fnemeet1  31332  curfv  32357  keridl  32799  pmapglbx  33871  elpaddn0  33902  paddasslem9  33930  paddasslem10  33931  cdleme42mgN  34592  relexpxpmin  36826  ntrclsk3  37186  n0p  38032  wessf1ornlem  38164  infxr  38323  lptre2pt  38506  dvnprodlem1  38635  fourierdlem42  38841  fourierdlem48  38846  fourierdlem54  38852  fourierdlem77  38875  sge0rpcpnf  39113  hoicvr  39237  cusgrrusgr  40778  upgrewlkle2  40805  wwlksm1edg  41075  clwwlksf  41219
  Copyright terms: Public domain W3C validator