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

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

Proof of Theorem ad4ant124
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expa 1117 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32adantlr 715 1 ((((𝜑𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  ad5ant124  1364  naddsuc2  8738  ixxin  13401  odf1  19595  m2cpmfo  22778  cnflf  24026  cnfcf  24066  tmdmulg  24116  blin  24447  blsscls2  24533  metcn  24572  xrsxmet  24845  sqf11  27197  dimval  33628  dfgcd3  37307  lindsadd  37600  hspmbllem2  46583
  Copyright terms: Public domain W3C validator