![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anbi1i | Structured version Visualization version Unicode version |
Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
Ref | Expression |
---|---|
3anbi1i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3anbi1i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anbi1i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | biid 240 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | biid 240 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3anbi123i 1196 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 189 df-an 373 df-3an 986 |
This theorem is referenced by: iinfi 7928 fzolb 11923 brfi1uzind 12648 opfi1uzind 12651 sqrlem5 13303 bitsmod 14403 isfunc 15762 txcn 20634 trfil2 20895 eulerpartlemn 29207 bnj976 29582 bnj543 29697 bnj594 29716 bnj917 29738 topdifinffinlem 31743 dath 33295 elfzolborelfzop1 40303 nnolog2flm1 40388 |
Copyright terms: Public domain | W3C validator |