![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expr | GIF version |
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Ref | Expression |
---|---|
expr.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
expr | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expr.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
2 | 1 | exp32 357 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp 122 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: reximddv 2465 rexlimdvaa 2479 issod 4082 ordsuc 4314 fcof1 5454 riota5f 5523 ovmpt2df 5663 tfrlemi1 5981 eqsuptid 6469 eqinftid 6493 ordiso2 6505 addnq0mo 6699 mulnq0mo 6700 genprndl 6773 genprndu 6774 addlocpr 6788 ltexprlemm 6852 ltexprlemopl 6853 ltexprlemopu 6855 ltexprlemfl 6861 ltexprlemfu 6863 aptiprleml 6891 caucvgprprlemexbt 6958 addsrmo 6982 mulsrmo 6983 prodge0 7999 un0addcl 8388 un0mulcl 8389 iseqfveq2 9544 iseqshft2 9548 monoord 9551 iseqsplit 9554 iseqid2 9564 expnegzap 9607 expcanlem 9740 ibcval5 9787 caucvgrelemcau 10004 cau3lem 10138 dvds0lem 10350 dvdsnegb 10357 dvdssub2 10382 isprm6 10670 |
Copyright terms: Public domain | W3C validator |