Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simprlr | GIF version |
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Ref | Expression |
---|---|
simprlr | ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antrl 482 | 1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: imain 5252 fcof1 5733 fliftfun 5746 sbthlemi6 6906 sbthlemi8 6908 addcmpblnq 7287 mulcmpblnq 7288 ordpipqqs 7294 enq0tr 7354 addcmpblnq0 7363 mulcmpblnq0 7364 nnnq0lem1 7366 addnq0mo 7367 mulnq0mo 7368 prarloclemcalc 7422 addlocpr 7456 distrlem4prl 7504 distrlem4pru 7505 addcmpblnr 7659 mulcmpblnrlemg 7660 mulcmpblnr 7661 prsrlem1 7662 addsrmo 7663 mulsrmo 7664 ltsrprg 7667 apreap 8462 apreim 8478 divdivdivap 8586 divsubdivap 8601 ledivdiv 8761 lediv12a 8765 exbtwnz 10150 seq3caopr 10382 leexp2r 10473 zfz1iso 10712 recvguniq 10895 rsqrmo 10927 summodclem2 11279 prodmodclem2 11474 prodmodc 11475 qredeu 11974 pw2dvdseu 12043 epttop 12501 txdis1cn 12689 metequiv2 12907 cncfmptc 12993 cncfmptid 12994 addccncf 12997 negcncf 12999 dedekindicclemicc 13021 |
Copyright terms: Public domain | W3C validator |