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

Theorem ad4ant14 1317
Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
Hypothesis
Ref Expression
ad4ant14.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad4ant14 ((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant14
StepHypRef Expression
1 ad4ant14.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 751 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
32adantlr 751 1 ((((𝜑𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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
This theorem is referenced by:  ad5ant14  1334  ad5ant15  1336  ad5ant25  1342  grprinvlem  6914  pntlem3  25343  hlpasch  25693  lfgrwlkprop  26640  wlkiswwlks1  26821  frgrnbnb  27273  frgr2wwlkeqm  27311  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem26  33565  mblfinlem2  33577  ssfiunibd  39837  xralrple2  39883  infleinf  39901  infxrpnf  39987  fprodcn  40150  limsupub  40254  limsuppnflem  40260  limsupmnflem  40270  cnrefiisplem  40373  climxlim2lem  40389  icccncfext  40418  cncficcgt0  40419  cncfioobd  40428  dvbdfbdioolem2  40462  itgspltprt  40513  stoweidlem34  40569  stoweidlem49  40584  stoweidlem57  40592  fourierdlem34  40676  fourierdlem39  40681  fourierdlem50  40691  fourierdlem51  40692  fourierdlem64  40705  fourierdlem73  40714  fourierdlem77  40718  fourierdlem81  40722  fourierdlem94  40735  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  fourier2  40762  etransclem24  40793  intsal  40866  sge0pr  40929  sge0iunmptlemfi  40948  sge0seq  40981  sge0reuz  40982  nnfoctbdjlem  40990  meadjiunlem  41000  ismeannd  41002  carageniuncllem2  41057  isomennd  41066  hoicvr  41083  hspmbllem2  41162  iunhoiioolem  41210  iunhoiioo  41211  vonioo  41217  vonicc  41220  preimageiingt  41251  preimaleiinlt  41252  smfaddlem1  41292  smfaddlem2  41293  smflimlem4  41303  smfrec  41317  smfinflem  41344  lighneallem3  41849  sprsymrelf1lem  42066
  Copyright terms: Public domain W3C validator