**Description:** Value of the conditional operator when its first argument is true.
(Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref | Expression | ||
---|---|---|---|

Hypothesis | iftrued.1 | ⊢ ( 𝜑 → 𝜒 ) | |

Assertion | iftrued | ⊢ ( 𝜑 → if ( 𝜒 , 𝐴 , 𝐵 ) = 𝐴 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | iftrued.1 | ⊢ ( 𝜑 → 𝜒 ) | |

2 | iftrue | ⊢ ( 𝜒 → if ( 𝜒 , 𝐴 , 𝐵 ) = 𝐴 ) | |

3 | 1 2 | syl | ⊢ ( 𝜑 → if ( 𝜒 , 𝐴 , 𝐵 ) = 𝐴 ) |