![]() |
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 560 | 1 ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: mpanl2 717 mpanr2 720 relopabi 5278 brprcneu 6222 mpt2eq12 6757 tfr3 7540 oaabslem 7768 omabslem 7771 isinf 8214 pssnn 8219 ige2m2fzo 12570 uzindi 12821 drsdirfi 16985 ga0 17777 lbsext 19211 lindfrn 20208 toprntopon 20777 fbssint 21689 filssufilg 21762 neiflim 21825 lmmbrf 23106 caucfil 23127 konigsbergssiedgwpr 27227 sspid 27708 onsucsuccmpi 32567 bj-restsn0 33163 bj-restn0 33168 poimirlem28 33567 lhpexle1 35612 diophun 37654 eldioph4b 37692 relexp1idm 38323 relexp0idm 38324 dvsid 38847 dvsef 38848 un10 39332 cnfex 39501 dvmptfprod 40478 |
Copyright terms: Public domain | W3C validator |