Theorem jctild 525

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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 512	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

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:  anc2li  555  equvini  2457  2reu1  3844  frpoinsg  6298  ordunidif  6364  isofrlem  7283  dfwe2  7716  orduniorsuc  7769  tfisg  7793  poxp  8067  fnse  8072  ssenen  9075  dffi3  9326  fpwwe2lem12  10544  zmulcl  12531  rpneg  12930  rexuz3  15263  cau3lem  15269  climrlim2  15461  o1rlimmul  15533  iseralt  15599  gcdzeq  16470  isprm3  16601  vdwnnlem2  16915  chnccat  18540  ablfaclem3  20009  epttop  22944  lmcnp  23239  dfconn2  23354  txcnp  23555  cmphaushmeo  23735  isfild  23793  cnpflf2  23935  flimfnfcls  23963  alexsubALT  23986  fgcfil  25218  bcthlem5  25275  ivthlem2  25400  ivthlem3  25401  dvfsumrlim  25985  plypf1  26164  noetalem1  27700  noseqinds  28243  axeuclidlem  28961  usgr2wlkneq  29755  wwlksnredwwlkn0  29895  wwlksnextwrd  29896  clwlkclwwlklem2a1  29993  lnon0  30799  hstles  32232  mdsl1i  32322  atcveq0  32349  atcvat4i  32398  cdjreui  32433  issgon  34208  connpconn  35351  outsideofrflx  36243  isbasisrelowllem1  37472  isbasisrelowllem2  37473  poimirlem3  37736  poimirlem29  37762  poimir  37766  heicant  37768  equivtotbnd  37891  ismtybndlem  37919  cvrat4  39615  linepsubN  39924  pmapsub  39940  osumcllem4N  40131  pexmidlem1N  40142  dochexmidlem1  41632  cantnfresb  43481  harval3  43695  clcnvlem  43780  relpfrlem  45110  iccpartimp  47579  sbgoldbwt  47939  sbgoldbst  47940  elsetrecslem  49860