![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl23anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl23anc.6 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) |
Ref | Expression |
---|---|
syl23anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | 1, 2 | jca 510 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl23anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 3, 4, 5, 6, 7 | syl13anc 1369 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: suppofss1d 8210 suppofss2d 8211 cnfcomlem 9724 ackbij1lem16 10260 div2subd 12073 symg2bas 19359 psgndiflemA 21550 evl1expd 22289 evls1maplmhm 22321 oftpos 22398 restopn2 23125 tsmsxp 24103 blcld 24458 cnllycmp 24926 dvlipcn 25971 tanregt0 26518 ostthlem1 27605 nosupbnd1lem1 27687 nosupbnd2 27695 noinfbnd1lem1 27702 noinfbnd2 27710 ax5seglem6 28817 axcontlem4 28850 axcontlem7 28853 wwlksnextwrd 29780 drngidlhash 33246 rhmpreimaprmidl 33263 qsdrngilem 33306 rsprprmprmidlb 33335 rprmirredb 33344 dfufd2lem 33364 lindsunlem 33453 pnfneige0 33683 qqhval2 33714 esumcocn 33830 carsgmon 34065 bnj1125 34754 heiborlem8 37422 2atjm 39048 1cvrat 39079 lvolnlelln 39187 lvolnlelpln 39188 4atlem3 39199 lplncvrlvol 39219 dalem39 39314 cdleme4a 39842 cdleme15 39881 cdleme16c 39883 cdleme19b 39907 cdleme19e 39910 cdleme20d 39915 cdleme20g 39918 cdleme20j 39921 cdleme20k 39922 cdleme20l2 39924 cdleme20l 39925 cdleme20m 39926 cdleme22e 39947 cdleme22eALTN 39948 cdleme22f 39949 cdleme27cl 39969 cdlemefr27cl 40006 mpaaeu 42716 |
Copyright terms: Public domain | W3C validator |