Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl2anb | Structured version Visualization version GIF version |
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
Ref | Expression |
---|---|
syl2anb.1 | ⊢ (𝜑 ↔ 𝜓) |
syl2anb.2 | ⊢ (𝜏 ↔ 𝜒) |
syl2anb.3 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
syl2anb | ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2anb.2 | . 2 ⊢ (𝜏 ↔ 𝜒) | |
2 | syl2anb.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | syl2anb.3 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylanb 583 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2b 595 | 1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: sylancb 601 rexdifi 4122 reupick3 4288 difprsnss 4732 opthhausdorff 5407 pwssun 5456 trin2 5983 sspred 6156 fundif 6403 fnun 6463 fco 6531 f1co 6585 foco 6602 f1oun 6634 f1oco 6637 eqfnfv 6802 eqfunfv 6807 sorpsscmpl 7460 ordsucsssuc 7538 ordsucun 7540 soxp 7823 ressuppssdif 7851 wfrlem4 7958 issmo 7985 tfrlem5 8016 ener 8556 domtr 8562 unen 8596 xpdom2 8612 mapen 8681 unxpdomlem3 8724 fiin 8886 suc11reg 9082 djuunxp 9350 xpnum 9380 pm54.43 9429 r0weon 9438 fseqen 9453 kmlem9 9584 axpre-lttrn 10588 axpre-mulgt0 10590 wloglei 11172 mulnzcnopr 11286 zaddcl 12023 zmulcl 12032 qaddcl 12365 qmulcl 12367 rpaddcl 12412 rpmulcl 12413 rpdivcl 12415 xrltnsym 12531 xrlttri 12533 xmullem 12658 xmulcom 12660 xmulneg1 12663 xmulf 12666 ge0addcl 12849 ge0mulcl 12850 ge0xaddcl 12851 ge0xmulcl 12852 serge0 13425 expclzlem 13454 expge0 13466 expge1 13467 hashfacen 13813 wwlktovf1 14321 qredeu 16002 nn0gcdsq 16092 mul4sq 16290 fpwipodrs 17774 pwmnd 18102 gimco 18408 gictr 18415 symgextf1 18549 efgrelexlemb 18876 xrs1mnd 20583 lmimco 20988 lmictra 20989 cctop 21614 iscn2 21846 iscnp2 21847 paste 21902 txuni 22200 txcn 22234 txcmpb 22252 tx2ndc 22259 hmphtr 22391 snfil 22472 supfil 22503 filssufilg 22519 tsmsxp 22763 dscmet 23182 rlimcnp 25543 efnnfsumcl 25680 efchtdvds 25736 lgsne0 25911 mul2sq 25995 colinearalglem2 26693 nb3grprlem2 27163 cplgr3v 27217 crctcshwlkn0 27599 wwlksnextinj 27677 hsn0elch 29025 shscli 29094 hsupss 29118 5oalem6 29436 mdsldmd1i 30108 superpos 30131 bnj110 32130 msubco 32778 poseq 33095 frrlem4 33126 sltsolem1 33180 fnsingle 33380 funimage 33389 funpartfun 33404 bj-nnfan 34077 bj-nnfor 34079 bj-snsetex 34278 bj-snmoore 34408 difunieq 34658 riscer 35281 divrngidl 35321 nn0rppwr 39202 nn0expgcd 39204 mzpincl 39351 kelac2lem 39684 cllem0 39945 unhe1 40151 tz6.12-1-afv 43393 tz6.12-1-afv2 43460 sprsymrelf1 43678 prmdvdsfmtnof1lem2 43767 uspgrsprf1 44042 2zrngamgm 44230 2zrngmmgm 44237 rrx2xpref1o 44725 |
Copyright terms: Public domain | W3C validator |