![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3ad2antl2 | Structured version Visualization version GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3ad2antl2 | ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
2 | 1 | adantlr 708 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
3 | 2 | 3adantl1 1213 | 1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 |
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 199 df-an 387 df-3an 1115 |
This theorem is referenced by: simpl2 1250 simpl2l 1303 simpl2r 1305 simpl21 1341 simpl22 1343 simpl23 1345 fcofo 6798 cocan1 6801 ordiso2 8689 fin1a2lem9 9545 fin1a2lem12 9548 gchpwdom 9807 winainflem 9830 bpolydif 15158 dvdsmodexp 15365 muldvds1 15383 lcmdvds 15694 ramcl 16104 gsumccat 17731 oddvdsnn0 18314 ghmplusg 18602 frlmsslss2 20481 frlmsslsp 20502 islindf4 20544 mamures 20563 matepmcl 20636 matepm2cl 20637 pmatcollpw2lem 20952 cnpnei 21439 ssref 21686 qtopss 21889 elfm2 22122 flffbas 22169 cnpfcf 22215 deg1ldg 24251 brbtwn2 26204 colinearalg 26209 axsegconlem1 26216 upgrpredgv 26438 cusgrrusgr 26879 upgrewlkle2 26904 wwlksm1edg 27180 wwlksm1edgOLD 27181 clwwlkfOLD 27392 clwwlkf 27397 wwlksext2clwwlk 27409 nvmul0or 28060 hoadddi 29217 volfiniune 30838 bnj548 31513 funsseq 32208 nn0prpwlem 32855 fnemeet1 32899 curfv 33932 lindsadd 33946 keridl 34373 pmapglbx 35844 elpaddn0 35875 paddasslem9 35903 paddasslem10 35904 cdleme42mgN 36563 relexpxpmin 38850 ntrclsk3 39208 n0p 40026 wessf1ornlem 40179 infxr 40380 lptre2pt 40667 dvnprodlem1 40956 fourierdlem42 41160 fourierdlem48 41165 fourierdlem54 41171 fourierdlem77 41194 sge0rpcpnf 41429 hoicvr 41556 smflimsuplem7 41826 isomgrsym 42554 |
Copyright terms: Public domain | W3C validator |