Theorem mpid 44

Description: A nested modus ponens deduction. Deduction associated with mpi 20. (Contributed by NM, 14-Dec-2004.)

Hypotheses

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

Assertion

Ref	Expression
mpid	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem mpid

Step	Hyp	Ref	Expression
1		mpid.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		mpid.2	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpdd 43	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mp2d  49  pm2.43a  54  embantd  59  mpan2d  693  ceqsalt  3474  rspcimdv  3561  riotass2  7123  peano5  7585  oeordi  8196  isf34lem4  9788  domtriomlem  9853  axcclem  9868  ssnn0fi  13348  repswrevw  14140  rlimcn1  14937  climcn1  14940  climcn2  14941  dvdsgcd  15882  lcmfunsnlem2lem1  15972  coprmgcdb  15983  nprm  16022  pcqmul  16180  prmgaplem7  16383  lubun  17725  grpid  18131  psgnunilem4  18617  gexdvds  18701  scmate  21115  cayleyhamilton1  21497  uniopn  21502  tgcmp  22006  uncmp  22008  nconnsubb  22028  comppfsc  22137  kgencn2  22162  isufil2  22513  cfinufil  22533  fin1aufil  22537  flimopn  22580  cnpflf  22606  flimfnfcls  22633  fcfnei  22640  metcnp3  23147  cncfco  23512  ellimc3  24482  dvfsumrlim  24634  cxploglim  25563  2sqreultblem  26032  nbuhgr2vtx1edgblem  27141  nbusgrvtxm1  27169  wlkp1lem6  27468  pthdlem2lem  27556  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  wlknwwlksnbij  27674  eupth2  28024  frgrncvvdeqlem8  28091  grpoid  28303  blocnilem  28587  htthlem  28700  nmcexi  29809  dmdbr3  30088  dmdbr4  30089  atom1d  30136  mclsax  32929  dfon2lem8  33148  nn0prpwlem  33783  bj-ceqsalt0  34324  bj-ceqsalt1  34325  filbcmb  35178  divrngidl  35466  lshpcmp  36284  lsat0cv  36329  atnle  36613  lpolconN  38783  ss2iundf  40360  iccpartdisj  43954  lighneallem2  44124  lighneallem3  44125  lighneallem4  44128  proththd  44132  sgoldbeven3prm  44301  bgoldbtbndlem2  44324  upgrwlkupwlk  44368  lindslinindsimp1  44866  nn0sumshdiglemA  45033  eenglngeehlnmlem2  45152  setrec1lem4  45220