![]() |
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 522 | 1 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: mpanl2 700 mpanr2 703 exan 1866 relopabi 5782 brprcneu 6836 brprcneuALT 6837 mpoeq12 7434 tfr3 8349 oaabslem 8597 omabslem 8600 enrefnn 8997 pssnn 9118 isinf 9210 isinfOLD 9211 pssnnOLD 9215 preleqALT 9561 ige2m2fzo 13644 uzindi 13896 drsdirfi 18202 ga0 19086 lbsext 20669 lindfrn 21250 toprntopon 22297 fbssint 23212 filssufilg 23285 neiflim 23348 lmmbrf 24649 caucfil 24670 lrrecfr 27284 konigsbergssiedgwpr 29242 sspid 29716 satfdmfmla 34058 satefvfmla1 34083 onsucsuccmpi 34968 bj-restn0 35611 poimirlem28 36156 lhpexle1 38521 diophun 41143 eldioph4b 41181 relexp1idm 42078 relexp0idm 42079 dvsid 42703 dvsef 42704 un10 43162 cnfex 43325 dvmptfprod 44276 |
Copyright terms: Public domain | W3C validator |