Theorem jctild 535

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctild.1	⊢ (𝜑 → (𝜓 → 𝜒))
jctild.2	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jctild	⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anc2li  565  equvini  2487  2reu1  3849  frpoinsg  6372  ordunidif  6439  isofrlem  7379  dfwe2  7820  orduniorsuc  7875  tfisg  7899  poxp  8177  fnse  8187  ssenen  9208  dffi3  9460  fpwwe2lem12  10766  zmulcl  12785  rpneg  13194  rexuz3  15560  cau3lem  15566  climrlim2  15758  o1rlimmul  15830  iseralt  15896  gcdzeq  16769  isprm3  16902  vdwnnlem2  17218  chnccat  18850  ablfaclem3  20354  epttop  23382  lmcnp  23677  dfconn2  23792  txcnp  23994  cmphaushmeo  24174  isfild  24232  cnpflf2  24374  flimfnfcls  24402  alexsubALT  24425  fgcfil  25647  bcthlem5  25704  ivthlem2  25828  ivthlem3  25829  dvfsumrlim  26406  plypf1  26586  noetalem1  28155  noseqinds  28736  axeuclidlem  29597  usgr2wlkneq  30399  wwlksnredwwlkn0  30542  wwlksnextwrd  30543  clwlkclwwlklem2a1  30640  lnon0  31457  hstles  32890  mdsl1i  32980  atcveq0  33007  atcvat4i  33056  cdjreui  33091  issgon  34866  onprcf1acwevdlem1  36086  onvfowev  36091  connpconn  36208  outsideofrflx  37107  isbasisrelowllem1  38546  isbasisrelowllem2  38547  poimirlem3  38809  poimirlem29  38835  poimir  38839  heicant  38841  equivtotbnd  38978  ismtybndlem  39006  cvrat4  40766  linepsubN  41075  pmapsub  41091  osumcllem4N  41282  pexmidlem1N  41293  dochexmidlem1  42783  cantnfresb  44587  harval3  44800  clcnvlem  44884  relpfrlem  46207  iccpartimp  48772  sbgoldbwt  49148  sbgoldbst  49149  elsetrecslem  51198