![]() |
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 714 | . 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
3 | 2 | 3adantl1 1164 | 1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 396 df-3an 1087 |
This theorem is referenced by: simpl2 1190 simpl2l 1224 simpl2r 1225 simpl21 1249 simpl22 1250 simpl23 1251 fcofo 7297 cocan1 7300 ordiso2 9538 fin1a2lem9 10431 fin1a2lem12 10434 gchpwdom 10693 winainflem 10716 bpolydif 16031 dvdsmodexp 16238 muldvds1 16257 lcmdvds 16578 ramcl 16997 oddvdsnn0 19498 ghmplusg 19800 frlmsslss2 21708 frlmsslsp 21729 islindf4 21771 mamures 22291 matepmcl 22363 matepm2cl 22364 pmatcollpw2lem 22678 cnpnei 23167 ssref 23415 qtopss 23618 elfm2 23851 flffbas 23898 cnpfcf 23944 deg1ldg 26027 brbtwn2 28715 colinearalg 28720 axsegconlem1 28727 upgrpredgv 28951 cusgrrusgr 29394 upgrewlkle2 29419 wwlksm1edg 29691 clwwlkf 29856 wwlksext2clwwlk 29866 nvmul0or 30459 hoadddi 31612 volfiniune 33849 bnj548 34528 funsseq 35363 nn0prpwlem 35806 fnemeet1 35850 curfv 37073 lindsadd 37086 keridl 37505 pmapglbx 39242 elpaddn0 39273 paddasslem9 39301 paddasslem10 39302 cdleme42mgN 39961 factwoffsmonot 41694 relexpxpmin 43147 ntrclsk3 43500 n0p 44407 wessf1ornlem 44558 infxr 44749 lptre2pt 45028 dvnprodlem1 45334 fourierdlem42 45537 fourierdlem48 45542 fourierdlem54 45548 fourierdlem77 45571 sge0rpcpnf 45809 hoicvr 45936 smflimsuplem7 46214 |
Copyright terms: Public domain | W3C validator |