Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > jcad | Structured version Visualization version GIF version |
Description: Deduction conjoining the consequents of two implications. Deduction form of jca 515 and double deduction form of pm3.2 473 and pm3.2i 474. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
Ref | Expression |
---|---|
jcad.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
jcad.2 | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Ref | Expression |
---|---|
jcad | ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jcad.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | jcad.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
3 | pm3.2 473 | . 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃))) | |
4 | 1, 2, 3 | syl6c 70 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: jca2 517 jctild 529 jctird 530 ancld 554 ancrd 555 oplem1 1057 2eu1 2651 2eu1v 2652 disjxiun 5050 iss 5903 oneqmini 6264 funssres 6424 elpreima 6878 isomin 7146 oneqmin 7584 frxp 7893 tposfo2 7991 oa00 8287 odi 8307 oneo 8309 oeordsuc 8322 oelim2 8323 nnarcl 8344 nnmord 8360 nnneo 8380 map0g 8565 pssnn 8846 onomeneq 8869 pssnnOLD 8895 fodomfib 8950 inf3lem4 9246 cplem1 9505 karden 9511 alephordi 9688 cardinfima 9711 dfac5lem5 9741 isf34lem4 9991 axcc4 10053 axdc3lem2 10065 zorn2lem4 10113 zorn2lem7 10116 indpi 10521 genpcl 10622 addclprlem2 10631 ltaddpr 10648 ltexprlem5 10654 suplem1pr 10666 ltlen 10933 dedekind 10995 mulgt1 11691 sup2 11788 nominpos 12067 uzind 12269 xrmaxlt 12771 xrltmin 12772 xrmaxle 12773 xrlemin 12774 xmullem2 12855 ccatopth 14281 shftuz 14632 sqreulem 14923 limsupbnd2 15044 mulcn2 15157 sadcaddlem 16016 dvdsgcdb 16105 algcvgblem 16134 lcmdvdsb 16170 rpexp 16279 infpnlem1 16463 divsfval 17052 iscatd 17176 posasymb 17826 plttr 17848 joinle 17892 meetle 17906 latnlej 17962 latnlej2 17965 lsmlub 19054 imasring 19637 unitmulclb 19683 lbspss 20119 lspsneu 20160 lspprat 20190 assapropd 20831 isclo2 21985 cncls2 22170 cncls 22171 cnntr 22172 cnrest2 22183 cmpsub 22297 cmpcld 22299 kgenss 22440 ptpjpre1 22468 txlm 22545 qtoptop2 22596 cmphaushmeo 22697 fbun 22737 isfild 22755 fbasrn 22781 fgtr 22787 ufinffr 22826 rnelfm 22850 fmfnfmlem4 22854 ghmcnp 23012 metrest 23422 icoopnst 23836 iocopnst 23837 dgreq0 25159 plyexmo 25206 cxpeq0 25566 mumullem2 26062 chpchtsum 26100 bposlem7 26171 lgsqr 26232 uspgr2wlkeq 27733 wwlknllvtx 27930 ex-natded5.3-2 28491 ubthlem1 28951 axhcompl-zf 29079 ococss 29374 nmopun 30095 elpjrn 30271 stm1addi 30326 stm1add3i 30328 mdsl1i 30402 chrelat2i 30446 atexch 30462 atcvat4i 30478 mdsymlem3 30486 bian1d 30528 bnj600 32612 subgrwlk 32807 pthacycspth 32832 subfacval2 32862 climuzcnv 33342 fundmpss 33459 soseq 33540 sltres 33602 nosupno 33643 noinfno 33658 segconeq 34049 ifscgr 34083 endofsegid 34124 colinbtwnle 34157 trer 34242 ivthALT 34261 fnessref 34283 fnemeet2 34293 fnejoin2 34295 onsuct0 34367 bj-ideqg1 35070 bj-elid6 35076 bj-finsumval0 35191 bj-isrvec2 35205 bj-bary1 35217 icorempo 35259 isbasisrelowllem1 35263 isbasisrelowllem2 35264 relowlpssretop 35272 finxpsuclem 35305 pibt2 35325 poimirlem31 35545 isbnd2 35678 bfplem2 35718 ghomco 35786 cnf1dd 35985 contrd 35992 mpobi123f 36057 mptbi12f 36061 iss2 36216 jca2r 36606 prter2 36632 lshpset2N 36870 cvrnbtwn2 37026 cvrnbtwn3 37027 cvrnbtwn4 37030 cvlcvr1 37090 hlrelat2 37154 cvrat4 37194 islpln2a 37299 linepsubN 37503 elpaddn0 37551 paddssw2 37595 pmapjoin 37603 ispsubcl2N 37698 dochkrshp 39137 dochsatshp 39202 mapdh9a 39540 hdmap11lem2 39593 frlmfzowrdb 39948 sn-sup2 40147 pwinfi3 40846 clsk1independent 41333 gneispace 41421 pm11.71 41688 2reu8i 44277 sbgoldbaltlem2 44905 setrec1lem4 46067 |
Copyright terms: Public domain | W3C validator |