![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad4antr | GIF version |
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad4antr | ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | ad3antrrr 479 | . 2 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
3 | 2 | adantr 272 | 1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: ad5antr 483 tfr1onlemaccex 6175 tfrcllemaccex 6188 fimax2gtri 6724 en2eqpr 6730 unsnfidcex 6737 unsnfidcel 6738 ctssdc 6912 cauappcvgprlemloc 7361 caucvgprlemm 7377 caucvgprlemladdrl 7387 caucvgprlemlim 7390 caucvgprprlemml 7403 caucvgprprlemexbt 7415 caucvgprprlemlim 7420 caucvgsrlemgt1 7490 axcaucvglemres 7584 xaddval 9469 rebtwn2zlemstep 9871 hashunlem 10391 caucvgre 10593 cvg1nlemres 10597 resqrexlemglsq 10634 maxabslemval 10820 xrmaxiflemcl 10853 xrmaxifle 10854 xrmaxiflemab 10855 xrmaxiflemlub 10856 xrmaxiflemval 10858 xrmaxltsup 10866 divalglemeunn 11413 dvdsbnd 11440 bezoutlemnewy 11477 bezoutlemmain 11479 txlm 12229 limcimo 12514 |
Copyright terms: Public domain | W3C validator |