|   | 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 520 | 1 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: mpanl2 701 mpanr2 704 exan 1861 relopabi 5831 brprcneu 6895 brprcneuALT 6896 mpoeq12 7507 tfr3 8440 oaabslem 8686 omabslem 8689 enrefnn 9088 pssnn 9209 isinf 9297 isinfOLD 9298 preleqALT 9658 ige2m2fzo 13768 uzindi 14024 drsdirfi 18352 ga0 19317 lbsext 21166 lindfrn 21842 toprntopon 22932 fbssint 23847 filssufilg 23920 neiflim 23983 lmmbrf 25297 caucfil 25318 lrrecfr 27977 konigsbergssiedgwpr 30269 sspid 30745 satfdmfmla 35406 satefvfmla1 35431 onsucsuccmpi 36445 bj-restn0 37092 poimirlem28 37656 lhpexle1 40011 diophun 42789 eldioph4b 42827 tfsconcatlem 43354 relexp1idm 43732 relexp0idm 43733 dvsid 44355 dvsef 44356 un10 44813 cnfex 45038 dvmptfprod 45965 | 
| Copyright terms: Public domain | W3C validator |