Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > impcomd | Structured version Visualization version GIF version |
Description: Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.) |
Ref | Expression |
---|---|
impd.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
impcomd | ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impd.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
2 | 1 | com23 86 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
3 | 2 | impd 411 | 1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: sbequ2 2240 sbequ2OLD 2241 ralxfrd 5299 ralxfrd2 5303 iss 5896 funssres 6391 fv3 6681 fmptsnd 6923 wfr3g 7942 nnmord 8247 cfcoflem 9682 nqereu 10339 ltletr 10720 fzind 12068 eqreznegel 12322 xrltletr 12538 xnn0xaddcl 12616 elfzodifsumelfzo 13091 hash2prde 13816 fundmge2nop0 13838 wrd2ind 14073 swrdccatin1 14075 rlimuni 14895 rlimno1 14998 ndvdssub 15748 lcmfunsnlem2 15972 coprmdvds 15985 coprmdvds2 15986 gsmsymgrfixlem1 18484 lsmdisj2 18737 chfacfisf 21390 chfacfisfcpmat 21391 lmcnp 21840 1stccnp 21998 txlm 22184 fgss2 22410 fgfil 22411 ufileu 22455 rnelfm 22489 fmfnfmlem2 22491 fmfnfmlem4 22493 ufilcmp 22568 cnpfcf 22577 alexsubALTlem2 22584 tsmsxp 22690 ivthlem2 23980 ivthlem3 23981 2sqreultlem 25950 2sqreultblem 25951 2sqreunnltlem 25953 2sqreunnltblem 25954 umgrislfupgrlem 26834 uhgr2edg 26917 wlkv0 27359 usgr2pth 27472 clwlkclwwlklem2 27705 frgrregord013 28101 prsrcmpltd 32244 sat1el2xp 32523 goalrlem 32540 dfpo2 32888 frrlem10 33029 |
Copyright terms: Public domain | W3C validator |