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 524 | 1 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: mpanl2 701 mpanr2 704 exan 1870 relopabi 5692 brprcneu 6708 fvprc 6709 mpoeq12 7284 tfr3 8135 oaabslem 8372 omabslem 8375 enrefnn 8724 pssnn 8846 isinf 8891 pssnnOLD 8895 preleqALT 9232 ige2m2fzo 13305 uzindi 13555 drsdirfi 17812 ga0 18692 lbsext 20200 lindfrn 20783 toprntopon 21822 fbssint 22735 filssufilg 22808 neiflim 22871 lmmbrf 24159 caucfil 24180 konigsbergssiedgwpr 28332 sspid 28806 satfdmfmla 33075 satefvfmla1 33100 lrrecfr 33837 onsucsuccmpi 34369 bj-restn0 34996 poimirlem28 35542 lhpexle1 37759 diophun 40298 eldioph4b 40336 relexp1idm 40999 relexp0idm 41000 dvsid 41622 dvsef 41623 un10 42081 cnfex 42244 dvmptfprod 43161 |
Copyright terms: Public domain | W3C validator |