Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ad4ant13 | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
Ref | Expression |
---|---|
ad4ant13.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad4ant13 | ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad4ant13.1 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 449 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | a1dd 48 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜒))) |
4 | 3 | a1d 25 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 → (𝜏 → 𝜒)))) |
5 | 4 | imp41 617 | 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 196 df-an 385 |
This theorem is referenced by: fntpb 6378 dvdslcmf 15182 trust 21843 metust 22173 matunitlindflem1 32575 mapss2 38392 supxrge 38495 xrlexaddrp 38509 infxr 38524 infleinf 38529 sge0isum 39320 sge0gtfsumgt 39336 sge0seq 39339 nnfoctbdjlem 39348 omeiunltfirp 39409 hspdifhsp 39506 hspmbllem2 39517 pimdecfgtioo 39604 pimincfltioo 39605 preimageiingt 39607 preimaleiinlt 39608 smfid 39639 proththd 40069 umgrres1lem 40529 upgrres1 40532 av-friendshipgt3 41552 |
Copyright terms: Public domain | W3C validator |