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

Theorem 3ad2antl2 1244
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 751 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl1 1237 1 (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  fcofo  6583  cocan1  6586  ordiso2  8461  fin1a2lem9  9268  fin1a2lem12  9271  gchpwdom  9530  winainflem  9553  bpolydif  14830  dvdsmodexp  15035  muldvds1  15053  lcmdvds  15368  ramcl  15780  gsumccat  17425  oddvdsnn0  18009  ghmplusg  18295  frlmsslss2  20162  frlmsslsp  20183  islindf4  20225  mamures  20244  matepmcl  20316  matepm2cl  20317  pmatcollpw2lem  20630  cnpnei  21116  ssref  21363  qtopss  21566  elfm2  21799  flffbas  21846  cnpfcf  21892  deg1ldg  23897  brbtwn2  25830  colinearalg  25835  axsegconlem1  25842  upgrpredgv  26079  cusgrrusgr  26533  upgrewlkle2  26558  wwlksm1edg  26835  clwwlkf  27010  wwlksext2clwwlk  27021  nvmul0or  27633  hoadddi  28790  volfiniune  30421  bnj548  31093  funsseq  31792  nn0prpwlem  32442  fnemeet1  32486  curfv  33519  keridl  33961  pmapglbx  35373  elpaddn0  35404  paddasslem9  35432  paddasslem10  35433  cdleme42mgN  36093  relexpxpmin  38326  ntrclsk3  38685  n0p  39523  wessf1ornlem  39685  infxr  39896  lptre2pt  40190  dvnprodlem1  40479  fourierdlem42  40684  fourierdlem48  40689  fourierdlem54  40695  fourierdlem77  40718  sge0rpcpnf  40956  hoicvr  41083  smflimsuplem7  41353
  Copyright terms: Public domain W3C validator