Metamath Proof Explorer


Theorem leexp1ad

Description: Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024)

Ref Expression
Hypotheses leexp1ad.1 φ A
leexp1ad.2 φ B
leexp1ad.3 φ N 0
leexp1ad.4 φ 0 A
leexp1ad.5 φ A B
Assertion leexp1ad φ A N B N

Proof

Step Hyp Ref Expression
1 leexp1ad.1 φ A
2 leexp1ad.2 φ B
3 leexp1ad.3 φ N 0
4 leexp1ad.4 φ 0 A
5 leexp1ad.5 φ A B
6 1 2 3 3jca φ A B N 0
7 6 4 5 jca32 φ A B N 0 0 A A B
8 leexp1a A B N 0 0 A A B A N B N
9 7 8 syl φ A N B N