![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jctr | Structured version Visualization version GIF version |
Description: Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
Ref | Expression |
---|---|
jctl.1 | ⊢ 𝜓 |
Ref | Expression |
---|---|
jctr | ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
2 | jctl.1 | . 2 ⊢ 𝜓 | |
3 | 1, 2 | jctir 521 | 1 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 397 |
This theorem is referenced by: mpanl2 699 mpanr2 702 exan 1865 relopabi 5776 brprcneu 6829 brprcneuALT 6830 mpoeq12 7424 tfr3 8337 oaabslem 8585 omabslem 8588 enrefnn 8949 pssnn 9070 isinf 9162 isinfOLD 9163 pssnnOLD 9167 preleqALT 9511 ige2m2fzo 13589 uzindi 13841 drsdirfi 18153 ga0 19036 lbsext 20576 lindfrn 21179 toprntopon 22225 fbssint 23140 filssufilg 23213 neiflim 23276 lmmbrf 24577 caucfil 24598 konigsbergssiedgwpr 29021 sspid 29495 satfdmfmla 33797 satefvfmla1 33822 lrrecfr 34251 onsucsuccmpi 34846 bj-restn0 35492 poimirlem28 36037 lhpexle1 38402 diophun 40998 eldioph4b 41036 relexp1idm 41890 relexp0idm 41891 dvsid 42515 dvsef 42516 un10 42974 cnfex 43137 dvmptfprod 44080 |
Copyright terms: Public domain | W3C validator |