| 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 410 | 1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: sbequ2 2249 ralxfrd 5408 ralxfrd2 5412 iss 6053 dfpo2 6316 funssres 6610 fv3 6924 fmptsnd 7189 resf1extb 7956 frrlem10 8320 wfr3g 8347 nnmord 8670 cfcoflem 10312 nqereu 10969 ltletr 11353 fzind 12716 eqreznegel 12976 xrltletr 13199 xnn0xaddcl 13277 elfzodifsumelfzo 13770 hash2prde 14509 hash3tpde 14532 fundmge2nop0 14541 wrd2ind 14761 swrdccatin1 14763 rlimuni 15586 rlimno1 15690 ndvdssub 16446 lcmfunsnlem2 16677 coprmdvds 16690 coprmdvds2 16691 gsmsymgrfixlem1 19445 lsmdisj2 19700 chfacfisf 22860 chfacfisfcpmat 22861 lmcnp 23312 1stccnp 23470 txlm 23656 fgss2 23882 fgfil 23883 ufileu 23927 rnelfm 23961 fmfnfmlem2 23963 fmfnfmlem4 23965 ufilcmp 24040 cnpfcf 24049 alexsubALTlem2 24056 tsmsxp 24163 ivthlem2 25487 ivthlem3 25488 2sqreultlem 27491 2sqreultblem 27492 2sqreunnltlem 27494 2sqreunnltblem 27495 negsid 28073 umgrislfupgrlem 29139 uhgr2edg 29225 wlkv0 29669 usgr2pth 29784 clwlkclwwlklem2 30019 frgrregord013 30414 prsrcmpltd 35095 sat1el2xp 35384 goalrlem 35401 isubgr3stgrlem7 47939 grlimgrtri 47963 |
| Copyright terms: Public domain | W3C validator |