Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  minmar1val Structured version   Unicode version

Theorem minmar1val 19442
 Description: Third substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
Hypotheses
Ref Expression
minmar1fval.a Mat
minmar1fval.b
minmar1fval.q minMatR1
minmar1fval.o
minmar1fval.z
Assertion
Ref Expression
minmar1val
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)

Proof of Theorem minmar1val
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 minmar1fval.a . . . 4 Mat
2 minmar1fval.b . . . 4
3 minmar1fval.q . . . 4 minMatR1
4 minmar1fval.o . . . 4
5 minmar1fval.z . . . 4
61, 2, 3, 4, 5minmar1val0 19441 . . 3
8 simp2 998 . . 3
9 simpl3 1002 . . 3
101, 2matrcl 19206 . . . . . . . 8
1110simpld 457 . . . . . . 7
1211, 11jca 530 . . . . . 6
13123ad2ant1 1018 . . . . 5
1413adantr 463 . . . 4
15 mpt2exga 6860 . . . 4
1614, 15syl 17 . . 3
17 eqeq2 2417 . . . . . . 7
1817adantr 463 . . . . . 6
19 eqeq2 2417 . . . . . . . 8
2019ifbid 3907 . . . . . . 7
2120adantl 464 . . . . . 6
2218, 21ifbieq1d 3908 . . . . 5
2322mpt2eq3dv 6344 . . . 4