Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ancrd | Structured version Visualization version GIF version |
Description: Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
Ref | Expression |
---|---|
ancrd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ancrd | ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancrd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | idd 24 | . 2 ⊢ (𝜑 → (𝜓 → 𝜓)) | |
3 | 1, 2 | jcad 516 | 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: impac 556 equvinva 2038 sbcg 3774 reuan 3808 2reu1 3809 reupick 4233 reusv2lem3 5293 ssrelrn 5763 relssres 5892 funmo 6396 funssres 6424 dffo4 6922 dffo5 6923 dfwe2 7559 ordpwsuc 7594 ordunisuc2 7623 dfom2 7646 nnsuc 7662 nnaordex 8366 wdom2d 9196 iundom2g 10154 fzospliti 13274 rexuz3 14912 qredeq 16214 prmdvdsfz 16262 dirge 18109 lssssr 19990 lpigen 20294 psgnodpm 20550 neiptopnei 22029 metustexhalf 23454 dyadmbllem 24496 3cyclfrgrrn2 28370 atexch 30462 ordtconnlem1 31588 bj-ideqg1 35070 bj-imdirval3 35090 isbasisrelowllem1 35263 isbasisrelowllem2 35264 pibt2 35325 phpreu 35498 poimirlem26 35540 sstotbnd3 35671 eqlkr3 36852 dihatexv 39089 dvh3dim2 39199 prjspner1 40171 neik0pk1imk0 41334 pm14.123b 41717 ordpss 41742 climreeq 42829 itscnhlc0xyqsol 45784 |
Copyright terms: Public domain | W3C validator |